From 7aec6c9ae7a54935ada0df0b4cc1efafc2291007 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 16 Jul 2024 09:43:26 +0200
Subject: [PATCH] chore: temporarily remove test broken by #4746

---
 tests/lean/ctor_layout.lean              | 18 ------------------
 tests/lean/ctor_layout.lean.expected.out | 15 ---------------
 2 files changed, 33 deletions(-)
 delete mode 100644 tests/lean/ctor_layout.lean
 delete mode 100644 tests/lean/ctor_layout.lean.expected.out

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
-◾