Commit 2021-05-14 00:28 8f76c3ba

View on Github →

feat(Util/Export): export format generator

Estimated changes

Created Mathlib/Util/Export.lean

added structure Lean.Export.Alloc

added inductive Lean.Export.Entry

added structure Lean.Export.State

added def Lean.Export.alloc

added def Lean.Export.biStr

added def Lean.Export.exportLevel

added def Lean.Export.exportName

added def Lean.Export.runExportM