A rudimentary export format, adapted from https://github.com/leanprover-community/lean/blob/master/doc/export_format.md with support for Lean 4 kernel primitives.

inductive Lean.Export.Entry : Type

• name (n : Name) : Entry
• level (n : Level) : Entry
• expr (n : Expr) : Entry
• defn (n : Name) : Entry

instance Lean.Export.instInhabitedEntry : Inhabited Entry

Equations

• Lean.Export.instInhabitedEntry = { default := Lean.Export.Entry.name default }

instance Lean.Export.instCoeNameEntry : Coe Name Entry

Equations

• Lean.Export.instCoeNameEntry = { coe := Lean.Export.Entry.name }

instance Lean.Export.instCoeLevelEntry : Coe Level Entry

Equations

• Lean.Export.instCoeLevelEntry = { coe := Lean.Export.Entry.level }

instance Lean.Export.instCoeExprEntry : Coe Expr Entry

Equations

• Lean.Export.instCoeExprEntry = { coe := Lean.Export.Entry.expr }

structure Lean.Export.Alloc (α : Type u_1) [BEq α] [Hashable α] : Type u_1

• map : Std.HashMap α Nat
• next : Nat

instance Lean.Export.instInhabitedAlloc {a✝ : Type u_1} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : Inhabited (Alloc a✝)

Equations

• Lean.Export.instInhabitedAlloc = { default := { map := default, next := default } }

structure Lean.Export.State : Type

• names : Alloc Name
• levels : Alloc Level
• exprs : Alloc Expr
• defs : Std.HashSet Name
• stk : Array (Bool × Entry)

instance Lean.Export.instInhabitedState : Inhabited State

Equations

• Lean.Export.instInhabitedState = { default := { names := default, levels := default, exprs := default, defs := default, stk := default } }

class Lean.Export.OfState (α : Type) [BEq α] [Hashable α] : Type

• get : State → Alloc α
• modify : (Alloc α → Alloc α) → State → State

instance Lean.Export.instOfStateName : OfState Name

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Export.instOfStateLevel : OfState Level

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Export.instOfStateExpr : OfState Expr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Lean.ExportM (α : Type) : Type

Equations

• Lean.ExportM = StateT Lean.Export.State Lean.CoreM

def Lean.Export.alloc {α : Type} [BEq α] [Hashable α] [OfState α] (a : α) : ExportM Nat

Equations

• One or more equations did not get rendered due to their size.

def Lean.Export.exportName (n : Name) : ExportM Nat

Equations

• One or more equations did not get rendered due to their size.
• Lean.Export.exportName Lean.Name.anonymous = do let __do_lift ← get match __do_lift.names.map[Lean.Name.anonymous]? with | some i => pure i | none => pure 0

def Lean.Export.exportLevel (L : Level) : ExportM Nat

Equations

• One or more equations did not get rendered due to their size.
• Lean.Export.exportLevel Lean.Level.zero = do let __do_lift ← get match __do_lift.levels.map[Lean.Level.zero]? with | some i => pure i | none => pure 0

def Lean.Export.biStr : BinderInfo → String

Equations

• Lean.Export.biStr Lean.BinderInfo.default = "#BD"
• Lean.Export.biStr Lean.BinderInfo.implicit = "#BI"
• Lean.Export.biStr Lean.BinderInfo.strictImplicit = "#BS"
• Lean.Export.biStr Lean.BinderInfo.instImplicit = "#BC"

partial def Lean.Export.exportExpr (E : Expr) : ExportM Nat

partial def Lean.Export.exportDef (n : Name) : ExportM Unit

def Lean.Export.exportDef.insert (n : Name) : ExportM Unit

Equations

• Lean.Export.exportDef.insert n = modify fun (s : Lean.Export.State) => { names := s.names, levels := s.levels, exprs := s.exprs, defs := s.defs.insert n, stk := s.stk }

partial def Lean.Export.exportDef.defn (ty : String) (n : Name) (t e : Expr) (ls : List Name) : ExportM Unit

partial def Lean.Export.exportDef.axdef (ty : String) (n : Name) (t : Expr) (ls : List Name) : ExportM Unit

partial def Lean.Export.exportDef.ind : List Name → ExportM Unit

partial def Lean.Export.exportDef.indbody (ind : Name) (s : String) : ExportM String

def Lean.Export.runExportM {α : Type} (m : ExportM α) : CoreM α

Equations

• Lean.Export.runExportM m = StateT.run' m default