Update informal.lean
This commit is contained in:
parent
5ede3718b6
commit
7b0ed296f5
1 changed files with 3 additions and 1 deletions
|
@ -168,7 +168,8 @@ unsafe def importToWebString (i : Import) : MetaM String := do
|
|||
pure ""
|
||||
else
|
||||
pure ("\n\n## " ++ i.module.toString ++ "\n" ++ String.intercalate "\n\n" informalPrint.toList)
|
||||
unsafe def main (args : List String) : IO Unit := do
|
||||
|
||||
unsafe def main (args : List String) : IO UInt32 := do
|
||||
initSearchPath (← findSysroot)
|
||||
let mods : Name := `HepLean
|
||||
let imp : Import := {module := mods}
|
||||
|
@ -186,3 +187,4 @@ unsafe def main (args : List String) : IO Unit := do
|
|||
let out := String.intercalate "\n" importWebString.toList
|
||||
IO.println (s!"Informal file made.")
|
||||
IO.FS.writeFile fileOut (informalFileHeader ++ out)
|
||||
pure 0
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue