From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- test-suite/success/refine.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 test-suite/success/refine.v (limited to 'test-suite/success/refine.v') diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v new file mode 100644 index 00000000..ad4eed5a --- /dev/null +++ b/test-suite/success/refine.v @@ -0,0 +1,30 @@ + +(* 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. + +(* Example submitted by Yves on coqdev *) + +Require PolyList. + +Goal (l:(list nat))l=l. +Proof. +Refine [l]<[l]l=l> + Cases l of + | nil => ? + | (cons O l0) => ? + | (cons (S _) l0) => ? + end. -- cgit v1.2.3