lean4-htt/tests/lean/reader1.lean.expected.out at f254a906b3dfe0785baf4f7b74b4ff32fef58baa - max/lean4-htt - maxgit: wireguard access, git repository.

max/lean4-htt

Sebastian Ullrich 6b6c16b6d6 chore(library/init/lean/parser/reader/module): remove theory command

We plan to allow `noncomputable`, as well as more modifiers, on `namespace/section`

2018-07-05 10:42:52 +02:00

9 lines

255 B

Text

Raw Blame History

 result:
 (module [(prelude "prelude")] [])
 result:
 (module [] [(import "import" [(import_path [] me)])])
 result:
 (module
  [(prelude "prelude")]
  [(import "import" [(import_path ["." "."] a) (import_path [] b)])
  (import "import" [(import_path [] c)])])