diff options
Diffstat (limited to 'test-suite/success/induct.v')
-rw-r--r-- | test-suite/success/induct.v | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 2aec6e9b..8e1a8d18 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -5,7 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Teste des definitions inductives imbriquees *) + +(* Test des definitions inductives imbriquees *) Require Import List. @@ -15,3 +16,28 @@ Inductive X : Set := Inductive Y : Set := cons2 : list (Y * Y) -> Y. +(* Test inductive types with local definitions *) + +Inductive eq1 : forall A:Type, let B:=A in A -> Prop := + refl1 : eq1 True I. + +Check + fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) => + let B := A in + fun (a : A) (e : eq1 A a) => + match e in (eq1 A0 B0 a0) return (P A0 a0) with + | refl1 => f + end. + +Inductive eq2 (A:Type) (a:A) + : forall B C:Type, let D:=(A*B*C)%type in D -> Prop := + refl2 : eq2 A a unit bool (a,tt,true). + +(* Check that induction variables are cleared even with in clause *) + +Lemma foo : forall n m : nat, n + m = n + m. +Proof. + intros; induction m as [|m] in n |- *. + auto. + auto. +Qed. |