40 lines
1.7 KiB
Text
40 lines
1.7 KiB
Text
[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.false 1
|
|
[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.true 2
|
|
[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.zero 1
|
|
[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.succ 1
|
|
[Compiler.floatLetIn] size: 11
|
|
def provokeFloatLet x y cond : Nat :=
|
|
let dual := Nat.mul x y
|
|
cases cond : Nat
|
|
| Bool.false =>
|
|
let b := Nat.add x y
|
|
let _x.1 := Nat.add b dual
|
|
_x.1
|
|
| Bool.true =>
|
|
cases dual : Nat
|
|
| Nat.zero =>
|
|
let a := Nat.pow x y
|
|
a
|
|
| Nat.succ n.2 =>
|
|
let c := Nat.sub x y
|
|
c
|
|
[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.false 0
|
|
[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.true 0
|
|
[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.zero 0
|
|
[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.succ 0
|
|
[Compiler.floatLetIn] size: 11
|
|
def provokeFloatLet x y cond : Nat :=
|
|
let dual := Nat.mul x y
|
|
cases cond : Nat
|
|
| Bool.false =>
|
|
let b := Nat.add x y
|
|
let _x.1 := Nat.add b dual
|
|
_x.1
|
|
| Bool.true =>
|
|
cases dual : Nat
|
|
| Nat.zero =>
|
|
let a := Nat.pow x y
|
|
a
|
|
| Nat.succ n.2 =>
|
|
let c := Nat.sub x y
|
|
c
|