diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /test-suite/success/Fixpoint.v | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'test-suite/success/Fixpoint.v')
-rw-r--r-- | test-suite/success/Fixpoint.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 680046da..cf821073 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -29,3 +29,22 @@ CoFixpoint g (n:nat) (m:=pred n) (l:Stream m) (p:=S n) : Stream p := Eval compute in (fun l => match g 2 (Consn 0 6 l) with Consn _ a _ => a end). +(* Check inference of simple types in presence of non ambiguous + dependencies (needs revision 10125) *) + +Section folding. + +Inductive vector (A:Type) : nat -> Type := + | Vnil : vector A 0 + | Vcons : forall (a:A) (n:nat), vector A n -> vector A (S n). + +Variables (B C : Set) (g : B -> C -> C) (c : C). + +Fixpoint foldrn n bs := + match bs with + | Vnil => c + | Vcons b _ tl => g b (foldrn _ tl) + end. + +End folding. + |