diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index 3afdb08f6f..85d8ef0305 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -113,7 +113,7 @@ def isErased : IRType → Bool | _ => false def boxed : IRType → IRType - | object | erased | float | float32 => object + | object | float | float32 => object | tagged | uint8 | uint16 => tagged | _ => tobject diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out index 33f1f1799e..7e4a5a9e2d 100644 --- a/tests/lean/computedFieldsCode.lean.expected.out +++ b/tests/lean/computedFieldsCode.lean.expected.out @@ -93,7 +93,7 @@ dec x_5; dec x_4; ret x_9 - def Exp.casesOn._override._boxed (x_1 : obj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) (x_9 : tobj) : tobj := + def Exp.casesOn._override._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) (x_9 : tobj) : tobj := let x_10 : tobj := Exp.casesOn._override x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9; dec x_9; dec x_8;