From a07e31a2693bde01d3dca59364693096d550561a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 11 Aug 2009 15:15:46 +0000
Subject: Ensures that let-in's in arities of inductive types work well. Maybe
 not very useful in practice but as soon as let-in's were not forbidden in the
 internal data structure, better to do it. Moreover, this gets closer to the
 view were inductive definitions are uniformly built from "contexts". (checker
 not changed!)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Inductive.v | 32 ++++++++++++++++++++++++++++++--
 test-suite/success/induct.v    | 19 ++++++++++++++++++-
 2 files changed, 48 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 1adcbd39a1..724ba502c7 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.
 
@@ -9,7 +37,7 @@ Check
    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) 
      (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).
 
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 2aec6e9b1c..1cf707583b 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,19 @@ 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).
-- 
cgit v1.2.3