Skip to content

Commit

Permalink
chore: revert "chore: temporarily remove test broken by leanprover#4746"
Browse files Browse the repository at this point in the history
This reverts commit 7aec6c9.
  • Loading branch information
Kha committed Aug 29, 2024
1 parent 44985dc commit cc458b8
Show file tree
Hide file tree
Showing 2 changed files with 33 additions and 0 deletions.
18 changes: 18 additions & 0 deletions tests/lean/ctor_layout.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
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
15 changes: 15 additions & 0 deletions tests/lean/ctor_layout.lean.expected.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
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

0 comments on commit cc458b8

Please sign in to comment.