Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
jpClosureIssue.lean
blob: c75d6d2e6f78599ddb6477c319dfc61ccb26cf04 [
file
] [
edit
]
@[
inline
]
def
f
(
b
:
Bool
)
:
IO
Nat
:=
match b
with
|
true
=>
return
0
|
false
=>
return
1
@[
noinline
]
def
print
(
x
:
Nat
)
:
IO
Unit
:=
IO
.
println x
set_option trace
.
Compiler
.
saveMono
true
def
foo
(
b
:
Bool
)
:
IO
Unit
:=
bind
(
f b
)
fun x
=>
print
x