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.

Instances For
    structure Lean.Export.Alloc (α : Type u_1) [BEq α] [Hashable α] :
    Type u_1
    Instances For
      instance Lean.Export.instInhabitedAlloc {a✝ : Type u_1} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} :
      Equations
      def Lean.Export.instInhabitedAlloc.default {a✝ : Type u_1} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} :
      Alloc a✝
      Equations
      Instances For
        Instances For
          class Lean.Export.OfState (α : Type) [BEq α] [Hashable α] :
          Instances
            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.
            @[reducible, inline]
            abbrev Lean.ExportM (α : Type) :
            Equations
            Instances For
              def Lean.Export.alloc {α : Type} [BEq α] [Hashable α] [OfState α] (a : α) :
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      partial def Lean.Export.exportDef.defn (ty : String) (n : Name) (t e : Expr) (ls : List Name) :
                      partial def Lean.Export.exportDef.axdef (ty : String) (n : Name) (t : Expr) (ls : List Name) :