Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/replace
/
.
/
tests
/
lean
/
603.lean
blob: 75b1f4a75e79cdb85a1f90b73ca3e66ea9dc7a51 [
file
] [
edit
]
set_option trace
.
compiler
.
ir
.
result
true
--
should be tail calls
mutual
partial
def
even
(
a
:
Nat
)
:
Nat
:=
if
a
==
0
then
1
else
odd
(
a
-
1
)
partial
def
odd
(
a
:
Nat
)
:
Nat
:=
if
a
==
0
then
0
else
even
(
a
-
1
)
end