diff options
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. + |