8 Commits

Author	SHA1	Message	Date
Guillaume Melquiond	46d53c02a9	Mark some types as having an extensional equality.	2024-11-13 19:04:52 +01:00
Claude Marche	c000797178	Additional operators for fmaps	2024-11-08 10:15:33 +01:00
MARCHE Claude	d37f66994a	after clone the axioms should be goals, not axioms	2024-02-29 13:33:13 +01:00
Guillaume Melquiond	ea123b5e95	Improve documentation of standard library.	2021-09-21 18:00:14 +02:00
Jean-Christophe Filliatre	1cbcc35a5f	library fmap: added a comment	2020-06-22 18:37:58 +02:00
Jean-Christophe Filliatre	1c43725a5e	fmap: notation [<-] for add, mapsto predicate	2019-11-19 16:05:46 +01:00
Jean-Christophe Filliatre	3dea26b887	set.SetAppInt/fmap.MapAppInt extracted to Set.Make and Map.Make ... fixed bugs in OCaml driver moved OCaml's exceptions Not_found and Exit to a separate module	2019-11-12 16:32:38 +01:00
Jean-Christophe Filliatre	253de0f125	stdlib: new library fmap ... fixes #283	2019-11-08 16:59:54 +01:00