structure DocGen4.Process.DocGenOptions : Type

• genEquations : Bool

@[reducible, inline]

abbrev DocGen4.Process.AnalyzeM : Type → Type

Equations

• DocGen4.Process.AnalyzeM = ReaderT DocGen4.Process.DocGenOptions Lean.MetaM

def DocGen4.Process.versoDocToMarkdown (v : Lean.VersoDocString) : String

Equations

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

structure DocGen4.Process.NameInfo : Type

Stores information about a typed name.

• name : Lean.Name

  The name that has this info attached.

• type : RenderedCode

  The pretty printed type of this name.

• doc : Option (String ⊕ Lean.VersoDocString)

  The doc string of the name if it exists.

@[implicit_reducible]

instance DocGen4.Process.instInhabitedNameInfo : Inhabited NameInfo

Equations

• DocGen4.Process.instInhabitedNameInfo = { default := DocGen4.Process.instInhabitedNameInfo.default }

structure DocGen4.Process.Arg : Type

An argument to a declaration, e.g. the (x : Nat) in def foo (x : Nat) := x.

• binder : RenderedCode

  The pretty printed binder syntax itself.

• implicit : Bool

  Whether the binder is implicit.

structure DocGen4.Process.Infoextends DocGen4.Process.NameInfo : Type

A base structure for information about a declaration.

• name : Lean.Name
• type : RenderedCode
• doc : Option (String ⊕ Lean.VersoDocString)
• args : Array Arg

  The list of arguments to the declaration.

• declarationRange : Lean.DeclarationRange

  In which lines the declaration was created.

• attrs : Array String

  A list of (known) attributes that are attached to the declaration.

• sorried : Bool

  Whether this declaration directly uses sorryAx.

• render : Bool

  Whether this info item should be rendered

@[implicit_reducible]

instance DocGen4.Process.instInhabitedInfo : Inhabited Info

Equations

• DocGen4.Process.instInhabitedInfo = { default := DocGen4.Process.instInhabitedInfo.default }

structure DocGen4.Process.AxiomInfoextends DocGen4.Process.Info : Type

Information about an axiom declaration.

• name : Lean.Name
• type : RenderedCode
• doc : Option (String ⊕ Lean.VersoDocString)
• args : Array Arg
• declarationRange : Lean.DeclarationRange
• attrs : Array String
• sorried : Bool
• render : Bool
• isUnsafe : Bool

@[implicit_reducible]

instance DocGen4.Process.instInhabitedAxiomInfo : Inhabited AxiomInfo

Equations

• DocGen4.Process.instInhabitedAxiomInfo = { default := DocGen4.Process.instInhabitedAxiomInfo.default }

structure DocGen4.Process.TheoremInfoextends DocGen4.Process.Info : Type

Information about a theorem declaration.

• name : Lean.Name
• type : RenderedCode
• doc : Option (String ⊕ Lean.VersoDocString)
• args : Array Arg
• declarationRange : Lean.DeclarationRange
• attrs : Array String
• sorried : Bool
• render : Bool

@[implicit_reducible]

instance DocGen4.Process.instInhabitedTheoremInfo : Inhabited TheoremInfo

Equations

• DocGen4.Process.instInhabitedTheoremInfo = { default := DocGen4.Process.instInhabitedTheoremInfo.default }

structure DocGen4.Process.OpaqueInfoextends DocGen4.Process.Info : Type

Information about an opaque declaration.

• name : Lean.Name
• type : RenderedCode
• doc : Option (String ⊕ Lean.VersoDocString)
• args : Array Arg
• declarationRange : Lean.DeclarationRange
• attrs : Array String
• sorried : Bool
• render : Bool
• definitionSafety : Lean.DefinitionSafety

  A value of partial is interpreted as this opaque being part of a partial def since the actual definition for a partial def is hidden behind an inaccessible value.

@[implicit_reducible]

instance DocGen4.Process.instInhabitedOpaqueInfo : Inhabited OpaqueInfo

Equations

• DocGen4.Process.instInhabitedOpaqueInfo = { default := DocGen4.Process.instInhabitedOpaqueInfo.default }

def DocGen4.Process.equationLimit : Nat

The maximum string length of equations before they are omitted from rendering.

This is an arbitrary cutoff that seems to work well in practice. Very long equations are unreadable in documentation and slow down page generation and rendering, so we drop them and show a notice instead. The number 200 has no deeper justification.

Equations exceeding this limit are stored as NULL blobs in the database (only text_length is preserved). The equationsWereOmitted field in DefinitionInfo is set when any equation exceeds this limit, causing the rendering code in DocGen4/Output/Definition.lean to show a notice.

Equations

• DocGen4.Process.equationLimit = 200

structure DocGen4.Process.DefinitionInfoextends DocGen4.Process.Info : Type

Information about a def declaration, note that partial defs are handled by OpaqueInfo.

• name : Lean.Name
• type : RenderedCode
• doc : Option (String ⊕ Lean.VersoDocString)
• args : Array Arg
• declarationRange : Lean.DeclarationRange
• attrs : Array String
• sorried : Bool
• render : Bool
• isUnsafe : Bool
• hints : Lean.ReducibilityHints
• equations : Option (Array RenderedCode)
• equationsWereOmitted : Bool
• isNonComputable : Bool

@[implicit_reducible]

instance DocGen4.Process.instInhabitedDefinitionInfo : Inhabited DefinitionInfo

Equations

• DocGen4.Process.instInhabitedDefinitionInfo = { default := DocGen4.Process.instInhabitedDefinitionInfo.default }

structure DocGen4.Process.InstanceInfoextends DocGen4.Process.DefinitionInfo : Type

Information about an instance declaration.

• name : Lean.Name
• type : RenderedCode
• doc : Option (String ⊕ Lean.VersoDocString)
• args : Array Arg
• declarationRange : Lean.DeclarationRange
• attrs : Array String
• sorried : Bool
• render : Bool
• isUnsafe : Bool
• hints : Lean.ReducibilityHints
• equations : Option (Array RenderedCode)
• equationsWereOmitted : Bool
• isNonComputable : Bool
• className : Lean.Name
• typeNames : Array Lean.Name

@[implicit_reducible]

instance DocGen4.Process.instInhabitedInstanceInfo : Inhabited InstanceInfo

Equations

• DocGen4.Process.instInhabitedInstanceInfo = { default := DocGen4.Process.instInhabitedInstanceInfo.default }

@[reducible, inline]

abbrev DocGen4.Process.ConstructorInfo : Type

Information about a constructor of an inductive type

Equations

• DocGen4.Process.ConstructorInfo = DocGen4.Process.Info

structure DocGen4.Process.InductiveInfoextends DocGen4.Process.Info : Type

Information about an inductive declaration

• name : Lean.Name
• type : RenderedCode
• doc : Option (String ⊕ Lean.VersoDocString)
• args : Array Arg
• declarationRange : Lean.DeclarationRange
• attrs : Array String
• sorried : Bool
• render : Bool
• ctors : List ConstructorInfo

  List of all constructors of this inductive type.

• isUnsafe : Bool

@[implicit_reducible]

instance DocGen4.Process.instInhabitedInductiveInfo : Inhabited InductiveInfo

Equations

• DocGen4.Process.instInhabitedInductiveInfo = { default := DocGen4.Process.instInhabitedInductiveInfo.default }

structure DocGen4.Process.FieldInfoextends DocGen4.Process.Info : Type

Stores information about a structure field.

• name : Lean.Name
• type : RenderedCode
• doc : Option (String ⊕ Lean.VersoDocString)
• args : Array Arg
• declarationRange : Lean.DeclarationRange
• attrs : Array String
• sorried : Bool
• render : Bool
• isDirect : Bool

  Whether or not this field is new to this structure, or instead whether it was inherited from a parent.

structure DocGen4.Process.StructureParentInfo : Type

Information about a structure parent.

• projFn : Lean.Name

  Name of the projection function.

• type : RenderedCode

  Pretty printed type.

structure DocGen4.Process.StructureInfoextends DocGen4.Process.Info : Type

Information about a structure declaration.

• name : Lean.Name
• type : RenderedCode
• doc : Option (String ⊕ Lean.VersoDocString)
• args : Array Arg
• declarationRange : Lean.DeclarationRange
• attrs : Array String
• sorried : Bool
• render : Bool
• fieldInfo : Array FieldInfo

  Information about all the fields of the structure.

• parents : Array StructureParentInfo

  All the structures this one inherited from.

• ctor : NameInfo

  The constructor of the structure.

@[implicit_reducible]

instance DocGen4.Process.instInhabitedStructureInfo : Inhabited StructureInfo

Equations

• DocGen4.Process.instInhabitedStructureInfo = { default := DocGen4.Process.instInhabitedStructureInfo.default }

@[reducible, inline]

abbrev DocGen4.Process.ClassInfo : Type

Information about a class declaration.

Equations

• DocGen4.Process.ClassInfo = DocGen4.Process.StructureInfo

@[reducible, inline]

abbrev DocGen4.Process.ClassInductiveInfo : Type

Information about a class inductive declaration.

Equations

• DocGen4.Process.ClassInductiveInfo = DocGen4.Process.InductiveInfo

inductive DocGen4.Process.DocInfo : Type

A general type for informations about declarations.

• axiomInfo (info : AxiomInfo) : DocInfo
• theoremInfo (info : TheoremInfo) : DocInfo
• opaqueInfo (info : OpaqueInfo) : DocInfo
• definitionInfo (info : DefinitionInfo) : DocInfo
• instanceInfo (info : InstanceInfo) : DocInfo
• inductiveInfo (info : InductiveInfo) : DocInfo
• structureInfo (info : StructureInfo) : DocInfo
• classInfo (info : ClassInfo) : DocInfo
• classInductiveInfo (info : ClassInductiveInfo) : DocInfo
• ctorInfo (info : ConstructorInfo) : DocInfo

@[implicit_reducible]

instance DocGen4.Process.instInhabitedDocInfo : Inhabited DocInfo

Equations

• DocGen4.Process.instInhabitedDocInfo = { default := DocGen4.Process.instInhabitedDocInfo.default }

def DocGen4.Process.DocInfo.toInfo : DocInfo → Info

Equations

• (DocGen4.Process.DocInfo.axiomInfo info).toInfo = info.toInfo
• (DocGen4.Process.DocInfo.theoremInfo info).toInfo = info.toInfo
• (DocGen4.Process.DocInfo.opaqueInfo info).toInfo = info.toInfo
• (DocGen4.Process.DocInfo.definitionInfo info).toInfo = info.toInfo
• (DocGen4.Process.DocInfo.instanceInfo info).toInfo = info.toInfo
• (DocGen4.Process.DocInfo.inductiveInfo info).toInfo = info.toInfo
• (DocGen4.Process.DocInfo.structureInfo info).toInfo = info.toInfo
• (DocGen4.Process.DocInfo.classInfo info).toInfo = info.toInfo
• (DocGen4.Process.DocInfo.classInductiveInfo info).toInfo = info.toInfo
• (DocGen4.Process.DocInfo.ctorInfo info).toInfo = info

def DocGen4.Process.prettyPrintTerm (expr : Lean.Expr) : Lean.MetaM RenderedCode

Turns an Expr into a pretty printed RenderedCode.

Equations

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

def DocGen4.Process.isInstance (declName : Lean.Name) : Lean.MetaM Bool

Equations

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