13 lines
117 B
Text
13 lines
117 B
Text
|
open nat
|
||
|
|
|
||
|
|
namespace foo
|
||
|
|
|
||
|
|
definition tst1 (a b : nat) : nat :=
|
||
|
|
match a with
|
||
|
|
| 0 := 1
|
||
|
|
| (n+1) := foo
|
||
|
|
end
|
||
|
|
|
||
|
|
|
||
|
|
end foo
|