diff options
| -rw-r--r-- | coq/example.v | 33 |
1 files changed, 1 insertions, 32 deletions
diff --git a/coq/example.v b/coq/example.v index 5d076280..d9976ea7 100644 --- a/coq/example.v +++ b/coq/example.v @@ -1,45 +1,14 @@ (* Example proof script for Coq Proof General. - This is a legal script for coq 7.x, with - imbricated proofs definitions. - - Replace Section by Module (>= coq-7.4). - $Id$ *) -Section sect. - Goal (A,B:Prop)(A /\ B) -> (B /\ A). Intros A B H. -Recursive Tactic Definition bar := Idtac. Elim H. Intros. - Lemma foo: (A:Set)Set. - Intro A. - Exact A. - Save. - Split. + Split. Assumption. Assumption. Save and_comms. -End sect. - -Section newmod. -Definition type1:=Set. - -Axiom A:False. -Goal (n:nat)(S n)=n. -Apply False_ind. -Exact A. -Save toto. -End newmod. - -Extract Constant - -Lemma Lem : (S O)=O. -AutoRewrite [db]. - -Hint Rewrite [toto] in db. -AutoRewrite [db]. |