diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 08:31:50 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 08:31:50 +0000 |
| commit | ca6bd6cdaaa05151408d927f5ebfc2b6bd156783 (patch) | |
| tree | c85bcc02a95ff30aad94b7bf270b12884e8774aa /test-suite/success | |
| parent | 618b18f7ae45c90062e5877cf55025ef5506b9b5 (diff) | |
Refine et let-in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2012 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/refine.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v new file mode 100644 index 000000000..1eb84a9be --- /dev/null +++ b/test-suite/success/refine.v @@ -0,0 +1,18 @@ + +(* Refine and let-in's *) + +Goal (EX x:nat | x=O). +Refine let y = (plus O O) in ?. +Exists y; Auto. +Save test1. + +Goal (EX x:nat | x=O). +Refine let y = (plus O O) in (ex_intro ? ? (plus y y) ?). +Auto. +Save test2. + +Goal nat. +Refine let y = O in (plus O ?). +Exact (S O). +Save test3. + |