Jean-Christophe Filliatre
|
4bc892fd02
|
a better theory seq.Sum
do not sum the elements, but rather the application of a
function to the elements
|
2025-12-03 19:01:11 +01:00 |
|
Claude Marche
|
cabea44347
|
fix realizations
|
2024-11-13 19:10:42 +01:00 |
|
MARCHE Claude
|
4d04b4f698
|
add metas for unused-dependencies on sequences
also fix split_full that was losing metas for unused dependency
|
2024-10-29 16:12:46 +01:00 |
|
Guillaume Melquiond
|
09a71c74c0
|
Fix occurrences of "occurences".
|
2023-11-23 19:04:11 +01:00 |
|
Jean-Christophe Filliatre
|
3e3bd79459
|
stdlib: fixed typo in seq.Sorted.sorted_append
|
2021-03-10 22:16:16 +01:00 |
|
Jean-Christophe Filliatre
|
e2fc9e23c3
|
libray seq: added a FIXME
|
2020-06-22 18:37:39 +02:00 |
|
Jean-Christophe Filliatre
|
0a950c3dac
|
library seq.Sorted uses TotalPreOrder, not TotalOrder
>
> fixes #336
|
2019-06-05 17:33:29 +02:00 |
|
Jean-Christophe Filliatre
|
661b93e911
|
library: added occ_all in seq.Occ
|
2019-06-05 15:48:32 +02:00 |
|
zapashcanon
|
03ba12028c
|
add missing lemmas about seq and occ
|
2019-06-05 15:19:41 +02:00 |
|
Jean-Christophe Filliatre
|
1aca8fe6fe
|
library: new theory seq.Sum
|
2019-05-08 22:30:01 +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
|
7b0929a761
|
WhyML: "use/clone T" imports by default (in absence of "as")
For the previous behaviour (no import), write "use/clone T as T".
This shortens the most used "use/clone import" to simply "use/clone".
|
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 |
|
Andrei Paskevich
|
bb165cfe46
|
Parser: rename [_.._] to [..] for consistency with other bracket ops
|
2018-06-05 15:36:43 +02:00 |
|
Jean-Christophe Filliatre
|
db64405b60
|
seq.Occ: minor change in the definition of occ
(name the lambda that is passed to numof)
|
2018-05-15 15:10:57 +02:00 |
|
Guillaume Melquiond
|
9e92f8203f
|
Change label syntax from "foo" to [@foo].
The feature is not yet fully implemented (e.g. escape characters).
|
2018-01-12 18:05:43 +01:00 |
|
Andrei Paskevich
|
85005b4f49
|
stdlib: rename *.why to *.mlw, use "module" instead of "theory"
|
2017-12-22 15:46:12 +01:00 |
|