diff --git a/src/Init/Lean/Compiler/IR/UnboxResult.lean b/src/Init/Lean/Compiler/IR/UnboxResult.lean index f29cad6559..818008c6f8 100644 --- a/src/Init/Lean/Compiler/IR/UnboxResult.lean +++ b/src/Init/Lean/Compiler/IR/UnboxResult.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura prelude import Init.Lean.Data.Format import Init.Lean.Compiler.IR.Basic -import Init.Lean.Compiler.IR.CtorLayout namespace Lean namespace IR