10 Commits

Author	SHA1	Message	Date
Jean-Christophe Filliatre	c928811d2d	map.MapPermut is a permutation	2025-05-07 23:43:38 +02:00
Guillaume Melquiond	46d53c02a9	Mark some types as having an extensional equality.	2024-11-13 19:04:52 +01:00
Jean-Christophe Filliatre	21a4cfe144	no more theory sum.Sum ... it is subsumed by theory int.Sum theories map.MapSum and array.ArraySum now use int.Sum	2020-02-12 10:30:25 +01:00
Jean-Christophe Filliatre	253de0f125	stdlib: new library fmap ... fixes #283	2019-11-08 16:59:54 +01:00
Andrei Paskevich	eae547d95f	stdlib, examples: remove redundant "import"	2018-06-15 16:45:58 +02:00
Andrei Paskevich	9e6dacc7ca	"safe clone": by default, cloned axioms become lemmas ... Clone "with axiom ." or "with goal ." to change the default ("with lemma ." is also accepted, just in case).	2018-06-14 21:44:44 +02:00
Guillaume Melquiond	1972035962	Convert the standard library.	2018-06-14 08:10:07 +02:00
Guillaume Melquiond	80e7237760	Generalize the statement of map.Occ.occ_exchange and realize it in Coq.	2018-03-13 16:52:25 +01:00
Jean-Christophe Filliatre	f2a36c56b6	stdlib: fixed lemma map.Occ.occ_exchange	2018-01-18 15:16:47 +01:00
Andrei Paskevich	85005b4f49	stdlib: rename *.why to *.mlw, use "module" instead of "theory"	2017-12-22 15:46:12 +01:00