blob: 6db5859b371e31e85be5d6d1ef0c02efc2b3d5f3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* Check keywords Conjecture and Admitted are recognized *)
Conjecture c : (n:nat)n=O.
Check c.
Theorem d : (n:nat)n=O.
Proof.
NewInduction n.
Reflexivity.
Assert H:False.
2:NewDestruct H.
Admitted.
|