blob: 0b40ef82a8fe3e1e040f04577bc0d8d771ef0c01 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Program Fixpoint f (a : nat) : nat :=
match a with
| 0 => 0
| S a' => g a a'
end
with g (a b : nat) { struct b } : nat :=
match b with
| 0 => 0
| S b' => f b'
end.
Check f.
Check g.
|