[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;
        return _x.1
      | Bool.true =>
        cases dual : Nat
        | Nat.zero =>
          let a := Nat.pow x y;
          return a
        | Nat.succ n.2 =>
          let c := Nat.sub x y;
          return 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;
        return _x.1
      | Bool.true =>
        cases dual : Nat
        | Nat.zero =>
          let a := Nat.pow x y;
          return a
        | Nat.succ n.2 =>
          let c := Nat.sub x y;
          return 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;
        return _x.1
      | Bool.true =>
        cases dual : Nat
        | Nat.zero =>
          let a := Nat.pow x y;
          return a
        | Nat.succ n.2 =>
          let c := Nat.sub x y;
          return c