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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
(* Treat "match" on a "cofix" like "match" on a constructor in guard condition *)
Module CofixRedex.
CoInductive Stream := {hd : nat; tl : Stream}.
Definition zeros := cofix zeros := {|hd := 0; tl := zeros|}.
Fixpoint f n :=
match n with
| 0 => 0
| S n =>
match zeros with
| {|hd:=_|} => fun f => f n
end f
end.
End CofixRedex.
Module CofixRedexPrimProj.
Set Primitive Projections.
CoInductive Stream A := {hd : A; tl : Stream A}.
Arguments hd {A} s.
Fixpoint f n :=
match n with
| 0 => 0
| S n => (cofix cst := {|hd := (fun f => f n); tl := cst|}).(hd) f
end.
End CofixRedexPrimProj.
(* Stack was missing when unfolding primitive projection in guard condition *)
Module ProjectionStack.
Set Primitive Projections.
Record T := { a : nat -> nat }.
Check fix f (b:bool) n : nat :=
match n with
| 0 => 0
| S n => (if b then {| a := f b |}.(a) else f b) n
end.
End ProjectionStack.
|
