lean4-htt/tests/lean/seqToCodeIssue.lean.expected.out
2022-10-15 15:48:02 -07:00

17 lines
579 B
Text

[Compiler.saveMono] size: 12
def f b a.1 : EStateM.Result IO.Error PUnit PUnit :=
jp _jp.2 a _y.3 : EStateM.Result IO.Error PUnit PUnit :=
let _x.4 := print a _y.3
cases _x.4 : EStateM.Result IO.Error PUnit PUnit
| EStateM.Result.ok a.5 a.6 =>
let _x.7 := print a a.6
_x.7
| EStateM.Result.error a.8 a.9 =>
_x.4
cases b : EStateM.Result IO.Error PUnit PUnit
| Bool.false =>
let a.10 := 1
goto _jp.2 a.10 a.1
| Bool.true =>
let a.11 := 0
goto _jp.2 a.11 a.1