bookshelf-doc/Main.lean

12 lines
291 B
Plaintext
Raw Normal View History

2021-11-27 15:19:56 +00:00
import DocGen4
import Lean
open DocGen4 Lean IO
2021-11-27 15:19:56 +00:00
def main (args : List String) : IO Unit := do
let modules := args
let path ← lakeSetupSearchPath (←getLakePath) modules.toArray
IO.println s!"Loading modules from: {path}"
let doc ← load $ modules.map Name.mkSimple
2021-11-27 15:19:56 +00:00
return ()