Documentation

Lean.PrettyPrinter.Delaborator.Metavariable

Utilities for pretty printing metavariables and generating dynamic docstrings #

source
def Lean.PrettyPrinter.Delaborator.delabMVarAux (m : MVarId) :
DelabM Term

Constructs a ?m term using the name of m or its index. Does not add terminfo. The metavariable does not need to be type correct in the current local context.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.PrettyPrinter.Delaborator.checkDelayedMVarAssignment (e : Expr) (decl : DelayedMetavarAssignment) :
    MetaM Bool

    Approximate check that the application ?m a₁ … aₙ of the delayed assignment metavariable ?m can be pretty printed using the pending metavariable.

    Heuristic: we assume the ldecl arguments are correct, and for the cdecls we check that they are distinct fvars

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      partial def Lean.PrettyPrinter.Delaborator.getDelayedMVarIdPending (mvarIdPending : MVarId) :
      MetaM MVarId

      Follows a chain of delayed assignments to find the pending metavariable.

      source
      def Lean.PrettyPrinter.Delaborator.mkDescribeMVar (mvarId : MVarId) (fromDelayed : Bool := false) :
      DelabM (PPContext → IO String)

      Creates an action that creates a description of the metavariable and its status in Markdown format, for use in the docstring in DelabTermInfo.

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