diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/success/induct.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
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. |