diff options
Diffstat (limited to 'test-suite/success/Inductive.v')
-rw-r--r-- | test-suite/success/Inductive.v | 27 |
1 files changed, 25 insertions, 2 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index f746def5..5b1482fd 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -64,7 +64,7 @@ Check (fun x:I1 => end). (* Check implicit parameters of inductive types (submitted by Pierre - Casteran and also implicit in #338) *) + Casteran and also implicit in BZ#338) *) Set Implicit Arguments. Unset Strict Implicit. @@ -80,7 +80,7 @@ Inductive Finite (A : Set) : LList A -> Prop := | Finite_LCons : forall (a : A) (l : LList A), Finite l -> Finite (LCons a l). -(* Check positivity modulo reduction (cf bug #983) *) +(* Check positivity modulo reduction (cf bug BZ#983) *) Record P:Type := {PA:Set; PB:Set}. @@ -183,3 +183,26 @@ Module PolyNoLowerProp. Fail Check Foo True : Prop. End PolyNoLowerProp. + +(* Test building of elimination scheme with noth let-ins and + non-recursively uniform parameters *) + +Module NonRecLetIn. + + Unset Implicit Arguments. + + Inductive Ind (b:=2) (a:nat) (c:=1) : Type := + | Base : Ind a + | Rec : Ind (S a) -> Ind a. + + Check Ind_rect (fun n (b:Ind n) => b = b) + (fun n => eq_refl) + (fun n b c => f_equal (Rec n) eq_refl) 0 (Rec 0 (Base 1)). + +End NonRecLetIn. + +(* Test treatment of let-in in the definition of Records *) +(* Should fail with "Sort expected" *) + +Fail Inductive foo (T : Type) : let T := Type in T := + { r : forall x : T, x = x }. |