diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-08 16:22:49 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-08 16:22:49 +0000 |
commit | 81afbd1e5682aa70625a47b3d0d00b3f312742ad (patch) | |
tree | e09a4829df80c38f21c5b049bbcae52c2c79f4a8 /test-suite/success/Inductive.v | |
parent | cbd10e42e2f9f75ded38cda1f96dc8fc5d8be98e (diff) |
Ajout exemple parametres implicites
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4551 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Inductive.v')
-rw-r--r-- | test-suite/success/Inductive.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 714fc19b5..87431a75c 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -17,3 +17,18 @@ Check f:((p0,q0:C)(P (Build_B C D x y p0 q0))); b:(B C D x y)] <[b0:(B C D x y)](P b0)>Cases b of (Build_B x0 x1) => (f x0 x1) end. + +(* Check implicit parameters of inductive types (submitted by Pierre + Casteran and also implicit in #338) *) + +Set Implicit Arguments. + +CoInductive LList [A:Set] : Set := + | LNil : (LList A) + | LCons : A -> (LList A) -> (LList A). + +Implicits LNil [1]. + +Inductive Finite [A:Set] : (LList A) -> Prop := + | Finite_LNil : (Finite LNil) + | Finite_LCons : (a:A) (l:(LList A)) (Finite l) -> (Finite (LCons a l)). |