| import init.lean.environment | |
| open Lean | |
| def saveTestFile (fn : String) : IO Unit := | |
| saveModuleData fn { | |
| imports := [`foo, `bla].toArray, | |
| constants := Array.empty, | |
| entries := Array.empty, | |
| serialized := [1, 2, 3, 4].toByteArray | |
| } | |
| def openTestFile (fn : String) : IO Unit := | |
| do m ← readModuleData fn, | |
| IO.println m.imports, | |
| IO.println m.serialized, | |
| pure () | |
| def main (xs : List String) : IO Unit := | |
| let fn := xs.head in | |
| saveTestFile fn *> | |
| openTestFile fn |