diff options
Diffstat (limited to 'test-suite/success/Inductive.v')
-rw-r--r-- | test-suite/success/Inductive.v | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 203fbbb7..da5dd5e4 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -54,6 +54,15 @@ Check | Build_B x0 x1 => f x0 x1 end). +(* Check inductive types with local definitions (constructors) *) + +Inductive I1 : Set := C1 (_:I1) (_:=0). + +Check (fun x:I1 => + match x with + | C1 i n => (i,n) + end). + (* Check implicit parameters of inductive types (submitted by Pierre Casteran and also implicit in #338) *) @@ -78,3 +87,23 @@ Record P:Type := {PA:Set; PB:Set}. Definition F (p:P) := (PA p) -> (PB p). Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F. + +(* Check that test for binders capturing implicit arguments is not stronger + than needed (problem raised by Cedric Auger) *) + +Set Implicit Arguments. +Inductive bool_comp2 (b: bool): bool -> Prop := +| Opp2: forall q, (match b return Prop with + | true => match q return Prop with + true => False | + false => True end + | false => match q return Prop with + true => True | + false => False end end) -> bool_comp2 b q. + +(* This one is still to be made acceptable... + +Set Implicit Arguments. +Inductive I A : A->Prop := C a : (forall A, A) -> I a. + + *) |