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