From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 test-suite/success/Inductive.v | 36 ++++++++++++++++++++++++++++++++----
 1 file changed, 32 insertions(+), 4 deletions(-)

(limited to 'test-suite/success/Inductive.v')

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 1adcbd39..203fbbb7 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -1,4 +1,32 @@
-(* Check local definitions in context of inductive types *)
+(* Test des definitions inductives imbriquees *)
+
+Require Import List.
+
+Inductive X : Set :=
+    cons1 : list X -> X.
+
+Inductive Y : Set :=
+    cons2 : list (Y * Y) -> Y.
+
+(* Test inductive types with local definitions (arity) *)
+
+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 inductive types with local definitions (parameters) *)
+
 Inductive A (C D : Prop) (E:=C) (F:=D) (x y : E -> F) : E -> Set :=
     I : forall z : E, A C D x y z.
 
@@ -7,9 +35,9 @@ Check
    let E := C in
    let F := D in
    fun (x y : E -> F) (P : forall c : C, A C D x y c -> Type)
-     (f : forall z : C, P z (I C D x y z)) (y0 : C) 
+     (f : forall z : C, P z (I C D x y z)) (y0 : C)
      (a : A C D x y y0) =>
-   match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with
+   match a as a0 in (A _ _ _ _ _ _ y1) return (P y1 a0) with
    | I x0 => f x0
    end).
 
@@ -20,7 +48,7 @@ Check
    let E := C in
    let F := D in
    fun (x y : E -> F) (P : B C D x y -> Type)
-     (f : forall p0 q0 : C, P (Build_B C D x y p0 q0)) 
+     (f : forall p0 q0 : C, P (Build_B C D x y p0 q0))
      (b : B C D x y) =>
    match b as b0 return (P b0) with
    | Build_B x0 x1 => f x0 x1
-- 
cgit v1.2.3