Documentation

Lean.Util.PPExt

structure Lean.PPContext :
Instances For
    @[reducible, inline]
    Equations
    Instances For

      A format tree with Elab.Info annotations. Each .tag n _ node is annotated with infos[n]. This is used to attach semantic data such as expressions to pretty-printer outputs.

      Instances For
        Equations
        • Lean.instInhabitedPPFns = { default := { ppExprWithInfos := default, ppTerm := default, ppLevel := default, ppGoal := default } }
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            Instances For
              Equations
              Instances For