test-suite/success/Conjecture.v


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.