[Compiler.simp] size: 9
    def f x b : Bool :=
      jp _jp.1 _y.2 : Bool :=
        let _x.3 := instDecidableEqNat x _y.2;
        let _x.4 := decide ◾ _x.3;
        return _x.4;
      cases b : Bool
      | Bool.false =>
        let _x.5 := 1;
        goto _jp.1 _x.5
      | Bool.true =>
        let _x.6 := 2;
        goto _jp.1 _x.6
[Compiler.simp] size: 9
    def f x b : Bool :=
      jp _jp.1 _y.2 : Bool :=
        let _x.3 := instDecidableEqNat x _y.2;
        let _x.4 := decide ◾ _x.3;
        return _x.4;
      cases b : Bool
      | Bool.false =>
        let _x.5 := 1;
        goto _jp.1 _x.5
      | Bool.true =>
        let _x.6 := 2;
        goto _jp.1 _x.6
[Compiler.simp] size: 9
    def f x b : Bool :=
      jp _jp.1 _y.2 : Bool :=
        let _x.3 := instDecidableEqNat x _y.2;
        let _x.4 := decide ◾ _x.3;
        return _x.4;
      cases b : Bool
      | Bool.false =>
        let _x.5 := 1;
        goto _jp.1 _x.5
      | Bool.true =>
        let _x.6 := 2;
        goto _jp.1 _x.6
[Compiler.simp] size: 7
    def f x b : Bool :=
      cases b : Bool
      | Bool.false =>
        let _x.1 := 1;
        let _x.2 := Nat.decEq x _x.1;
        return _x.2
      | Bool.true =>
        let _x.3 := 2;
        let _x.4 := Nat.decEq x _x.3;
        return _x.4
[Compiler.simp] size: 7
    def f x b : Bool :=
      cases b : Bool
      | Bool.false =>
        let _x.1 := 1;
        let _x.2 := Nat.decEq x _x.1;
        return _x.2
      | Bool.true =>
        let _x.3 := 2;
        let _x.4 := Nat.decEq x _x.3;
        return _x.4
[Compiler.simp] size: 7
    def f x b : Bool :=
      cases b : Bool
      | Bool.false =>
        let _x.1 := 1;
        let _x.2 := Nat.decEq x _x.1;
        return _x.2
      | Bool.true =>
        let _x.3 := 2;
        let _x.4 := Nat.decEq x _x.3;
        return _x.4
[Compiler.simp] size: 12
    def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
      let _x.2 := "f";
      let _x.3 := Lean.Name.mkStr1 _x.2;
      let _x.4 := 1;
      let _x.5 := @Array.mkEmpty _ _x.4;
      let _x.6 := @Array.push _ _x.5 _x.3;
      let _x.7 := PUnit.unit;
      fun _f.8 _y.9 @&_y.10 @&_y.11 @&_y.12 @&_y.13 @&_y.14 _y.15 : EST.Out Lean.Exception lcAny PUnit :=
        let _x.16 := Lean.Compiler.compile _x.6 _y.13 _y.14 _y.15;
        cases _x.16 : EST.Out Lean.Exception lcAny PUnit
        | EST.Out.ok a.17 a.18 =>
          let _x.19 := @EST.Out.ok _ _ _ _x.7 a.18;
          return _x.19
        | EST.Out.error a.20 a.21 =>
          return _x.16;
      let _x.22 := @Lean.Elab.Command.liftTermElabM _ _f.8 a a a.1;
      return _x.22
[Compiler.simp] size: 12
    def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
      let _x.2 := "f";
      let _x.3 := Lean.Name.mkStr1 _x.2;
      let _x.4 := 1;
      let _x.5 := @Array.mkEmpty _ _x.4;
      let _x.6 := @Array.push _ _x.5 _x.3;
      let _x.7 := PUnit.unit;
      fun _f.8 _y.9 @&_y.10 @&_y.11 @&_y.12 @&_y.13 @&_y.14 _y.15 : EST.Out Lean.Exception lcAny PUnit :=
        let _x.16 := Lean.Compiler.compile _x.6 _y.13 _y.14 _y.15;
        cases _x.16 : EST.Out Lean.Exception lcAny PUnit
        | EST.Out.ok a.17 a.18 =>
          let _x.19 := @EST.Out.ok _ _ _ _x.7 a.18;
          return _x.19
        | EST.Out.error a.20 a.21 =>
          return _x.16;
      let _x.22 := @Lean.Elab.Command.liftTermElabM _ _f.8 a a a.1;
      return _x.22
[Compiler.simp] size: 12
    def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
      let _x.2 := "f";
      let _x.3 := Lean.Name.mkStr1 _x.2;
      let _x.4 := 1;
      let _x.5 := @Array.mkEmpty _ _x.4;
      let _x.6 := @Array.push _ _x.5 _x.3;
      let _x.7 := PUnit.unit;
      fun _f.8 _y.9 @&_y.10 @&_y.11 @&_y.12 @&_y.13 @&_y.14 _y.15 : EST.Out Lean.Exception lcAny PUnit :=
        let _x.16 := Lean.Compiler.compile _x.6 _y.13 _y.14 _y.15;
        cases _x.16 : EST.Out Lean.Exception lcAny PUnit
        | EST.Out.ok a.17 a.18 =>
          let _x.19 := @EST.Out.ok _ _ _ _x.7 a.18;
          return _x.19
        | EST.Out.error a.20 a.21 =>
          return _x.16;
      let _x.22 := @Lean.Elab.Command.liftTermElabM _ _f.8 a a a.1;
      return _x.22
[Compiler.simp] size: 12
    def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
      let _x.2 := "f";
      let _x.3 := Lean.Name.mkStr1 _x.2;
      let _x.4 := 1;
      let _x.5 := Array.mkEmpty ◾ _x.4;
      let _x.6 := Array.push ◾ _x.5 _x.3;
      let _x.7 := PUnit.unit;
      fun _f.8 _y.9 @&_y.10 @&_y.11 @&_y.12 @&_y.13 @&_y.14 _y.15 : EST.Out Lean.Exception lcAny PUnit :=
        let _x.16 := Lean.Compiler.compile _x.6 _y.13 _y.14 _y.15;
        cases _x.16 : EST.Out Lean.Exception lcAny PUnit
        | EST.Out.ok a.17 a.18 =>
          let _x.19 := @EST.Out.ok ◾ ◾ ◾ _x.7 a.18;
          return _x.19
        | EST.Out.error a.20 a.21 =>
          return _x.16;
      let _x.22 := Lean.Elab.Command.liftTermElabM._redArg _f.8 a a a.1;
      return _x.22
[Compiler.simp] size: 12
    def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
      let _x.2 := "f";
      let _x.3 := Lean.Name.mkStr1 _x.2;
      let _x.4 := 1;
      let _x.5 := Array.mkEmpty ◾ _x.4;
      let _x.6 := Array.push ◾ _x.5 _x.3;
      let _x.7 := PUnit.unit;
      fun _f.8 _y.9 @&_y.10 @&_y.11 @&_y.12 @&_y.13 @&_y.14 _y.15 : EST.Out Lean.Exception lcAny PUnit :=
        let _x.16 := Lean.Compiler.compile _x.6 _y.13 _y.14 _y.15;
        cases _x.16 : EST.Out Lean.Exception lcAny PUnit
        | EST.Out.ok a.17 a.18 =>
          let _x.19 := @EST.Out.ok ◾ ◾ ◾ _x.7 a.18;
          return _x.19
        | EST.Out.error a.20 a.21 =>
          return _x.16;
      let _x.22 := Lean.Elab.Command.liftTermElabM._redArg _f.8 a a a.1;
      return _x.22
[Compiler.simp] size: 5
    def _private.elab.attachJp.0._eval._lam_0 _x.1 _x.2 _y.3 @&_y.4 @&_y.5 @&_y.6 @&_y.7 @&_y.8 _y.9 : EST.Out
      Lean.Exception lcAny PUnit :=
      let _x.10 := Lean.Compiler.compile _x.1 _y.7 _y.8 _y.9;
      cases _x.10 : EST.Out Lean.Exception lcAny PUnit
      | EST.Out.ok a.11 a.12 =>
        let _x.13 := @EST.Out.ok ◾ ◾ ◾ _x.2 a.12;
        return _x.13
      | EST.Out.error a.14 a.15 =>
        return _x.10
[Compiler.simp] size: 8
    def _private.elab.attachJp.0._eval @&a @&a a.1 : EST.Out Lean.Exception lcAny PUnit :=
      let _x.2 := "f";
      let _x.3 := Lean.Name.mkStr1 _x.2;
      let _x.4 := 1;
      let _x.5 := Array.mkEmpty ◾ _x.4;
      let _x.6 := Array.push ◾ _x.5 _x.3;
      let _x.7 := PUnit.unit;
      let _f.8 := _eval._lam_0 _x.6 _x.7;
      let _x.9 := Lean.Elab.Command.liftTermElabM._redArg _f.8 a a a.1;
      return _x.9