# 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.

@[inline]
Equations
def Lean.PrettyPrinter.Delaborator.SubExpr.getExpr {m : } [inst : ] [inst : ] :
Equations
• Lean.PrettyPrinter.Delaborator.SubExpr.getExpr = do let __do_lift ← pure __do_lift.expr
def Lean.PrettyPrinter.Delaborator.SubExpr.getPos {m : } [inst : ] [inst : ] :
Equations
• Lean.PrettyPrinter.Delaborator.SubExpr.getPos = do let __do_lift ← pure __do_lift.pos
def Lean.PrettyPrinter.Delaborator.SubExpr.descend {α : Type} {m : } [inst : ] (child : Lean.Expr) (childIdx : Nat) (x : m α) :
m α
Equations
def Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn {α : Type} {m : } [inst : ] [inst : ] [inst : ] (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
def Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg {α : Type} {m : } [inst : ] [inst : ] [inst : ] (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
def Lean.PrettyPrinter.Delaborator.SubExpr.withType {α : Type} {m : } [inst : ] [inst : ] [inst : ] [inst : ] (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.PrettyPrinter.Delaborator.SubExpr.withAppFnArgs {α : Type} {m : } [inst : ] [inst : ] [inst : ] (xf : m α) (xa : αm α) :
m α
def Lean.PrettyPrinter.Delaborator.SubExpr.withBindingDomain {α : Type} {m : } [inst : ] [inst : ] [inst : ] (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
def Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody {α : Type} {m : } [inst : ] [inst : ] [inst : ] [inst : ] (n : Lean.Name) (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
def Lean.PrettyPrinter.Delaborator.SubExpr.withProj {α : Type} [inst : ] {m : } [inst : ] [inst : ] [inst : ] (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
def Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr {α : Type} [inst : ] {m : } [inst : ] [inst : ] [inst : ] (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
def Lean.PrettyPrinter.Delaborator.SubExpr.withLetVarType {α : Type} [inst : ] {m : } [inst : ] [inst : ] [inst : ] (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
def Lean.PrettyPrinter.Delaborator.SubExpr.withLetValue {α : Type} [inst : ] {m : } [inst : ] [inst : ] [inst : ] (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
def Lean.PrettyPrinter.Delaborator.SubExpr.withLetBody {α : Type} [inst : ] {m : } [inst : ] [inst : ] [inst : ] [inst : ] (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
def Lean.PrettyPrinter.Delaborator.SubExpr.withNaryFn {α : Type} {m : } [inst : ] [inst : ] [inst : ] (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
def Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg {α : Type} {m : } [inst : ] [inst : ] [inst : ] (argIdx : Nat) (x : m α) :
m α
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.

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.