diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-06-19 12:17:28 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-06-19 12:17:28 +0000 |
| commit | 0b1e882fb3489c98206cb780065b46276c082bc6 (patch) | |
| tree | dbd6ac985fa94ce4ea8c463d2a40e762b50897fc /etc/coq | |
| parent | 6f2bea55f4a6c14f9233a8c9c4280e7d00042053 (diff) | |
Added End for sections, and silly test
Diffstat (limited to 'etc/coq')
| -rw-r--r-- | etc/coq/nested.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/etc/coq/nested.v b/etc/coq/nested.v index 53a84c10..ab2af6c6 100644 --- a/etc/coq/nested.v +++ b/etc/coq/nested.v @@ -40,6 +40,7 @@ Fixpoint f [n:nat] : nat := Cases n of O => O | (S m)=> (f m) end. (* 2b. Retraction to 2a from here uses "Reset". Retraction to 2a from inside proof uses "Abort. Back." *) + Lemma t1: (n: nat ) {n=O} + {(EX y | n = (S y))}. (* 3 This needs "Restart" to be retracted if inside the proof, and "Reset t1. Back 4." if outside (after point 12). 3 because of the @@ -73,8 +74,12 @@ Intros. (* 9 "Undo": example of retraction 9->6: Undo 2. Back 3. *) EAuto. (* 11 "Undo" *) Save. (* 12 *) - +End Apple. Section Banana. +Lemma Coq: O=O. Auto. Save. (* silly example to show that testing + prompt to determine if we're in proof + mode is not good enough. *) +End Banana. |