blob: 387cacdf3cd5c111d7397855e7fe20fcfeab25bf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
TODO
----
- axiomes pour les prédicats récursifs comme
Fixpoint even (n:nat) : Prop :=
match n with
O => True
| S O => False
| S (S p) => even p
end.
ou encore In sur les listes du module Coq List.
- discriminate
- inversion (Set et Prop)
BUGS
----
- value = Some : forall A:Set, A -> option A
-> eta_expanse échoue sur assert false (ligne 147)
|
