Def Lean.Export.runExportM

Modification history

2024-07-13 12:38
Mathlib/Util/Export.lean
chore: remove autoImplicit in Util (#14694) …
Modified Lean.Export.runExportMView on Github →
2022-01-17 11:03
Mathlib/Util/Export.lean
chore: bump to nightly-2022-01-17 (#160)
Modified Lean.Export.runExportMView on Github →
2021-05-14 00:28
Mathlib/Util/Export.lean
feat(Util/Export): export format generator
Added Lean.Export.runExportMView on Github →