lean4-htt/tests/lean/run/spec_issue.lean
Leonardo de Moura 8383177c96 fix: nonoptimal specialization
@Kha Here is the fix for the problem I told you this morning.
Please, take a look at `specialize.cpp` and see whether it makes sense.
2020-09-24 12:40:28 -07:00

7 lines
168 B
Text

new_frontend
set_option trace.compiler.ir.result true
def g (ys : List Nat) : IO Nat := do
let x := 0;
(_, x) ← StateT.run (ys.forM fun y => IO.println y) x;
pure x