diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean deleted file mode 100644 index e9b7c43daa..0000000000 --- a/tests/lean/ctor_layout.lean +++ /dev/null @@ -1,18 +0,0 @@ -import Lean.Compiler.IR - -open Lean -open Lean.IR - -unsafe def main : IO Unit := -withImportModules #[{module := `Lean.Compiler.IR.Basic}] {} 0 fun env => do - let ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse; - ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo); - IO.println "---"; - let ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.EnvironmentHeader.mk; - ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo); - IO.println "---"; - let ctorLayout ← IO.ofExcept $ getCtorLayout env `Subtype.mk; - ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo); - pure () - -#eval main diff --git a/tests/lean/ctor_layout.lean.expected.out b/tests/lean/ctor_layout.lean.expected.out deleted file mode 100644 index f15ad0f679..0000000000 --- a/tests/lean/ctor_layout.lean.expected.out +++ /dev/null @@ -1,15 +0,0 @@ -obj@0 -obj@1 -scalar#1@0:u8 -obj@2 ---- -scalar#4@0:u32 -scalar#1@4:u8 -obj@0 -obj@1 -obj@2 -obj@3 -obj@4 ---- -obj@0 -◾