plugins/dp/TODO


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24


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
----