diff options
Diffstat (limited to 'test-suite/success/PatternsInBinders.v')
-rw-r--r-- | test-suite/success/PatternsInBinders.v | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/test-suite/success/PatternsInBinders.v b/test-suite/success/PatternsInBinders.v new file mode 100644 index 00000000..77710791 --- /dev/null +++ b/test-suite/success/PatternsInBinders.v @@ -0,0 +1,67 @@ +(** The purpose of this file is to test functional properties of the + destructive patterns used in binders ([fun] and [forall]). *) + + +Definition swap {A B} '((x,y) : A*B) := (y,x). + +(** Tests the use of patterns in [fun] and [Definition] *) +Section TestFun. + + Variables A B : Type. + + Goal forall (x:A) (y:B), swap (x,y) = (y,x). + Proof. reflexivity. Qed. + + Goal forall u:A*B, swap (swap u) = u. + Proof. destruct u. reflexivity. Qed. + + Goal @swap A B = fun '(x,y) => (y,x). + Proof. reflexivity. Qed. + +End TestFun. + + +(** Tests the use of patterns in [forall] *) +Section TestForall. + + Variables A B : Type. + + Goal forall '((x,y) : A*B), swap (x,y) = (y,x). + Proof. intros [x y]. reflexivity. Qed. + + Goal forall x0:A, exists '((x,y) : A*A), swap (x,y) = (x,y). + Proof. + intros x0. + exists (x0,x0). + reflexivity. + Qed. + +End TestForall. + + + +(** Tests the use of patterns in dependent definitions. *) + +Section TestDependent. + + Inductive Fin (n:nat) := Z : Fin n. + + Definition F '(n,p) : Type := (Fin n * Fin p)%type. + + Definition both_z '(n,p) : F (n,p) := (Z _,Z _). + +End TestDependent. + + +(** Tests with a few other types just to make sure parsing is + robust. *) +Section TestExtra. + + Definition proj_informative {A P} '(exist _ x _ : { x:A | P x }) : A := x. + + Inductive Foo := Bar : nat -> bool -> unit -> nat -> Foo. + + Definition foo '(Bar n b tt p) := + if b then n+p else n-p. + +End TestExtra. |