Documentation

Lean.PrettyPrinter.Delaborator.SubExpr

Subexpr utilities for delaborator. #

This file defines utilities for MetaM computations to traverse subexpressions of an expression in sync with the Nat "position" values that refer to them.

Equations
Instances For
    Equations
    Instances For
      def Lean.PrettyPrinter.Delaborator.SubExpr.descend {α : Type} {m : TypeType} [MonadWithReaderOf Lean.SubExpr m] (child : Lean.Expr) (childIdx : Nat) (x : m α) :
      m α
      Equations
      Instances For
        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
            • One or more equations did not get rendered due to their size.
            Instances For
              partial def Lean.PrettyPrinter.Delaborator.SubExpr.withAppFnArgs {α : Type} {m : TypeType} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (xf : m α) (xa : αm α) :
              m α
              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
                  • 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
                      • 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
                          • 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
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                The positioning scheme guarantees that there will be an infinite number of extra positions which are never used by Exprs. The HoleIterator always points at the next such "hole". We use these to attach additional Elab.Info.

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