max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update script/reformat.lean

Browse source
This commit is contained in:
Sebastian Ullrich 2022-05-13 11:55:44 +02:00
parent 5cd4bd3552
commit 4934104eaf
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
script/reformat.lean
View file

@ -59,10 +59,11 @@ def parseModule (input : String) (fileName : String) (opts : Options := {}) (tru
pure {env, currNamespace, openDecls, stx}
| _ =>
failWith "unknown info tree"
#[{ env := env0, stx := header : CommandSyntax }] ++ topLevelCmds
return #[{ env := env0, stx := header : CommandSyntax }] ++ topLevelCmds
unsafe def main (args : List String) : IO Unit := do
let [fileName] ← args | failWith "Usage: reformat file"
let [fileName] := args | failWith "Usage: reformat file"
initSearchPath (← findSysroot)
let input ← IO.FS.readFile fileName
let moduleStx ← parseModule input fileName
let leadingUpdated := mkNullNode (moduleStx.map (·.stx)) |>.updateLeading |>.getArgs