Def Lean.Export.exportLevel

Modification history

2021-05-14 00:28
Mathlib/Util/Export.lean
feat(Util/Export): export format generator
Added Lean.Export.exportLevelView on Github →