Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
seqToCodeIssue.lean
blob: 5c785ba615b1386cffcc8a6fc769834f5f430bd7 [
file
] [
edit
]
@[
noinline
]
def
print
(
n
:
Nat
)
:
IO
Unit
:=
IO
.
println n
set_option trace
.
Compiler
.
saveMono
true
def
f
(
b
:
Bool
)
:
IO
Unit
:=
do
let
a
:
Nat
←
match b
with
|
true
=>
pure
0
|
false
=>
pure
1
print
a
print
a