Documentation

Mathlib.Util.Export

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.

structure Lean.Export.Alloc (α : Type u_1) [inst : BEq α] [inst : Hashable α] :
Type u_1
Instances For
    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 } }
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    def Lean.Export.alloc {α : Type} [inst : BEq α] [inst : Hashable α] [inst : Lean.Export.OfState α] (a : α) :
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Equations