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.
- name: Lean.Name → Lean.Export.Entry
- level: Lean.Level → Lean.Export.Entry
- expr: Lean.Expr → Lean.Export.Entry
- defn: Lean.Name → Lean.Export.Entry
Instances For
- map : Lean.HashMap α Nat
- next : Nat
Instances For
instance
Lean.Export.instInhabitedAlloc :
{a : Type u_1} → {a_1 : BEq a} → {a_2 : Hashable a} → Inhabited (Lean.Export.Alloc a)
- 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)
Instances For
- get : Lean.Export.State → Lean.Export.Alloc α
- modify : (Lean.Export.Alloc α → Lean.Export.Alloc α) → Lean.Export.State → Lean.Export.State
Instances
Instances For
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
Instances For
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