zapashcanon
f722d1d3dd
Add safe_peek and safe_pop in all pqueue modules
2019-07-03 16:11:41 +02:00
Jean-Christophe Filliatre
309be35d9c
library: several changes in pqueue
...
- both Pqueue and PqueueNoDup now require a TotalPreOrder, not TotalOrder
- Pqueue now modeled using sequences instead of lists
- a harness module for Pqueue (external heapsort)
- both Pqueue and PqueueNoDup now have coercions
2019-07-02 17:07:21 +02:00
Jean-Christophe Filliatre
8a7974cf74
stdlib: set library revamped
2019-03-07 11:13:49 +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
efb51e7d43
Merge theories and modules into stdlib (fix issue #62 ).
2017-12-15 15:34:35 +01:00
