blob: b9181d430a1171dbf22db25d2411a6814ae70e54 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* Specific tests about guard condition *)
(* f must unfold to x, not F (de Bruijn mix-up!) *)
Check let x (f:nat->nat) k := f k in
fun (y z:nat->nat) =>
let f:=x in (* f := Rel 3 *)
fix F (n:nat) : nat :=
match n with
| 0 => 0
| S k => f F k (* here Rel 3 = F ! *)
end.
|
