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

def Lean.Export.instInhabitedEntry.default : Entry

@[implicit_reducible]

instance Lean.Export.instInhabitedEntry : Inhabited Entry

@[implicit_reducible]

instance Lean.Export.instCoeNameEntry : Coe Name Entry

@[implicit_reducible]

instance Lean.Export.instCoeLevelEntry : Coe Level Entry

@[implicit_reducible]

instance Lean.Export.instCoeExprEntry : Coe Expr Entry

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

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

@[implicit_reducible]

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

def Lean.Export.instInhabitedAlloc.default {a✝ : Type u_1} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : Alloc a✝

structure Lean.Export.State : Type

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

def Lean.Export.instInhabitedState.default : State

@[implicit_reducible]

instance Lean.Export.instInhabitedState : Inhabited State

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

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

@[implicit_reducible]

instance Lean.Export.instOfStateName : OfState Name

@[implicit_reducible]

instance Lean.Export.instOfStateLevel : OfState Level

@[implicit_reducible]

instance Lean.Export.instOfStateExpr : OfState Expr

@[reducible, inline]

abbrev Lean.ExportM (α : Type) : Type

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

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

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

def Lean.Export.biStr : BinderInfo → String

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

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

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