blob: 680046da4c573b2a0560a5ceddd1f16888901d98 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
(* Playing with (co-)fixpoints with local definitions *)
Inductive listn : nat -> Set :=
niln : listn 0
| consn : forall n:nat, nat -> listn n -> listn (S n).
Fixpoint f (n:nat) (m:=pred n) (l:listn m) (p:=S n) {struct l} : nat :=
match n with O => p | _ =>
match l with niln => p | consn q _ l => f (S q) l end
end.
Eval compute in (f 2 (consn 0 0 niln)).
CoInductive Stream : nat -> Set :=
Consn : forall n, nat -> Stream n -> Stream (S n).
CoFixpoint g (n:nat) (m:=pred n) (l:Stream m) (p:=S n) : Stream p :=
match n return (let m:=pred n in forall l:Stream m, let p:=S n in Stream p)
with
| O => fun l:Stream 0 => Consn O 0 l
| S n' =>
fun l:Stream n' =>
let l' :=
match l in Stream q return Stream (pred q) with Consn _ _ l => l end
in
let a := match l with Consn _ a l => a end in
Consn (S n') (S a) (g n' l')
end l.
Eval compute in (fun l => match g 2 (Consn 0 6 l) with Consn _ a _ => a end).
|
