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) [BEq α] [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)
    @[inline, reducible]
    abbrev Lean.ExportM (α : Type) :
    Instances For
      Instances For
        Equations
        Instances For
          Equations
          Instances For
            Instances For