def DocGen4.Process.valueToEq (v : Lean.DefinitionVal) : Lean.MetaM Lean.Expr

Equations

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

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

Equations

• DocGen4.Process.prettyPrintEquation expr = Lean.Meta.forallTelescope expr.consumeMData fun (x : Array Lean.Expr) (e : Lean.Expr) => DocGen4.Process.prettyPrintTerm e

def DocGen4.Process.processEq (eq : Lean.Name) : Lean.MetaM RenderedCode

Equations

• DocGen4.Process.processEq eq = do let type ← Lean.Meta.mkConstWithFreshMVarLevels eq >>= Lean.Meta.inferType DocGen4.Process.prettyPrintEquation type

def DocGen4.Process.computeEquations? (v : Lean.DefinitionVal) : AnalyzeM (Array RenderedCode)

Equations

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

def DocGen4.Process.DefinitionInfo.ofDefinitionVal (v : Lean.DefinitionVal) : AnalyzeM DefinitionInfo

Equations

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