From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- test-suite/success/Inductive.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) (limited to 'test-suite/success/Inductive.v') 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. + + *) -- cgit v1.2.3