diff options
| -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 0000000000..1eb84a9bef --- /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. + |