diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean index 27c6093123..e0d06e672a 100644 --- a/src/Lean/Compiler/IR/ToIR.lean +++ b/src/Lean/Compiler/IR/ToIR.lean @@ -208,7 +208,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do return code else mkExpr (.fap name irArgs) - else if let some scalarType ← lowerEnumToScalarType? ctorVal.name then + else if let some scalarType ← lowerEnumToScalarType? ctorVal.induct then assert! args.isEmpty let var ← bindVar decl.fvarId return .vdecl var scalarType (.lit (.num ctorVal.cidx)) (← lowerCode k) diff --git a/tests/lean/4240.lean.expected.out b/tests/lean/4240.lean.expected.out index 4693783eb0..83a83e685f 100644 --- a/tests/lean/4240.lean.expected.out +++ b/tests/lean/4240.lean.expected.out @@ -2,13 +2,11 @@ def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 (x_1 : @& obj) : u8 := case x_1 : obj of MyOption.none → - let x_2 : obj := ctor_0[Bool.false]; - let x_3 : u8 := unbox x_2; - ret x_3 + let x_2 : u8 := 0; + ret x_2 MyOption.some → - let x_4 : obj := ctor_1[Bool.true]; - let x_5 : u8 := unbox x_4; - ret x_5 + let x_3 : u8 := 1; + ret x_3 def isSomeWithInstanceNat (x_1 : @& obj) : u8 := let x_2 : usize := 0; let x_3 : obj := Array.uget ◾ x_1 x_2 ◾; diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out index 9bf7a277c6..6452a084e6 100644 --- a/tests/lean/computedFieldsCode.lean.expected.out +++ b/tests/lean/computedFieldsCode.lean.expected.out @@ -175,13 +175,11 @@ def g (x_1 : @& obj) : u8 := case x_1 : obj of Exp.a3._impl → - let x_2 : obj := ctor_1[Bool.true]; - let x_3 : u8 := unbox x_2; - ret x_3 + let x_2 : u8 := 1; + ret x_2 default → - let x_4 : obj := ctor_0[Bool.false]; - let x_5 : u8 := unbox x_4; - ret x_5 + let x_3 : u8 := 0; + ret x_3 def g._boxed (x_1 : obj) : obj := let x_2 : u8 := g x_1; dec x_1;