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.

ink

inductive Lean.Export.Entry : Type

• name: Lean.Name → Lean.Export.Entry
• level: Lean.Level → Lean.Export.Entry
• expr: Lean.Expr → Lean.Export.Entry
• defn: Lean.Name → Lean.Export.Entry

ink

instance Lean.Export.instInhabitedEntry : Inhabited Lean.Export.Entry

Equations

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

ink

instance Lean.Export.instCoeNameEntry : Coe Lean.Name Lean.Export.Entry

Equations

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

ink

instance Lean.Export.instCoeLevelEntry : Coe Lean.Level Lean.Export.Entry

Equations

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

ink

instance Lean.Export.instCoeExprEntry : Coe Lean.Expr Lean.Export.Entry

Equations

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

ink

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

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

ink

instance Lean.Export.instInhabitedAlloc : {a : Type u_1} → {a_1 : BEq a} → {a_2 : Hashable a} → Inhabited (Lean.Export.Alloc a)

Equations

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

ink

structure Lean.Export.State : Type

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

ink

instance Lean.Export.instInhabitedState : Inhabited Lean.Export.State

Equations

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

ink

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

• get : Lean.Export.State → Lean.Export.Alloc α
• modify : (Lean.Export.Alloc α → Lean.Export.Alloc α) → Lean.Export.State → Lean.Export.State

ink

instance Lean.Export.instOfStateNameInstBEqNameInstHashableName : Lean.Export.OfState Lean.Name

Equations

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

ink

instance Lean.Export.instOfStateLevelInstBEqLevelInstHashableLevel : Lean.Export.OfState Lean.Level

Equations

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

ink

instance Lean.Export.instOfStateExprInstBEqExprInstHashableExpr : Lean.Export.OfState Lean.Expr

Equations

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

ink

@[inline]

abbrev Lean.ExportM (α : Type) : Type

Equations

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

ink

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

Equations

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

ink

def Lean.Export.exportName (n : Lean.Name) : Lean.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 Lean.HashMap.find? __do_lift.names.map Lean.Name.anonymous with | some i => pure i | none => pure 0

ink

def Lean.Export.exportLevel (L : Lean.Level) : Lean.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 Lean.HashMap.find? __do_lift.levels.map Lean.Level.zero with | some i => pure i | none => pure 0

ink

def Lean.Export.biStr : Lean.BinderInfo → String

Equations

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

ink

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

ink

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

ink

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

Equations

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

ink

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

ink

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

ink

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

ink

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

ink

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

Equations

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