1
(* Playing with (co-)fixpoints with local definitions *)
3
Inductive listn : nat -> Set :=
5
| consn : forall n:nat, nat -> listn n -> listn (S n).
7
Fixpoint f (n:nat) (m:=pred n) (l:listn m) (p:=S n) {struct l} : nat :=
8
match n with O => p | _ =>
9
match l with niln => p | consn q _ l => f (S q) l end
12
Eval compute in (f 2 (consn 0 0 niln)).
14
CoInductive Stream : nat -> Set :=
15
Consn : forall n, nat -> Stream n -> Stream (S n).
17
CoFixpoint g (n:nat) (m:=pred n) (l:Stream m) (p:=S n) : Stream p :=
18
match n return (let m:=pred n in forall l:Stream m, let p:=S n in Stream p)
20
| O => fun l:Stream 0 => Consn O 0 l
24
match l in Stream q return Stream (pred q) with Consn _ _ l => l end
26
let a := match l with Consn _ a l => a end in
27
Consn (S n') (S a) (g n' l')
30
Eval compute in (fun l => match g 2 (Consn 0 6 l) with Consn _ a _ => a end).
32
(* Check inference of simple types in presence of non ambiguous
33
dependencies (needs revision 10125) *)
37
Inductive vector (A:Type) : nat -> Type :=
39
| Vcons : forall (a:A) (n:nat), vector A n -> vector A (S n).
41
Variables (B C : Set) (g : B -> C -> C) (c : C).
43
Fixpoint foldrn n bs :=
46
| Vcons b _ tl => g b (foldrn _ tl)