diff options
Diffstat (limited to 'coq/example.v')
-rw-r--r-- | coq/example.v | 32 |
1 files changed, 27 insertions, 5 deletions
diff --git a/coq/example.v b/coq/example.v index 5a3c5b59..5d55a2ae 100644 --- a/coq/example.v +++ b/coq/example.v @@ -1,14 +1,36 @@ (* 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. - Induction H. - Apply conj. - Assumption. - Assumption. + Intros A B H. +Recursive Tactic Definition bar := Idtac. + Elim H. + Intros. + Lemma foo: (A:Set)Set. + Intro A. + Exact A. + Save. + Split. + Assumption. + Assumption. Save and_comms. +End sect. + +Module mod. +Definition type1:=Set. +End mod. + +Module Type newmod. +Definition type1:=Set. +End newmod. |