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.

source
@[inline]
abbrev Lean.PrettyPrinter.Delaborator.OptionsPerPos:
Type
Equations
source
def Lean.PrettyPrinter.Delaborator.SubExpr.getExpr {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] :
m Lean.Expr
Equations
source
def Lean.PrettyPrinter.Delaborator.SubExpr.getPos {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] :
m Lean.SubExpr.Pos
Equations
source
def Lean.PrettyPrinter.Delaborator.SubExpr.descend {α : Type} {m : Type → Type} [inst : MonadWithReaderOf Lean.SubExpr m] (child : Lean.Expr) (childIdx : Nat) (x : m α) :
m α
Equations
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn {α : Type} {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] (x : m α) :
m α
Equations
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg {α : Type} {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] (x : m α) :
m α
Equations
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withType {α : Type} {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] [inst : MonadLiftT Lean.MetaM m] (x : m α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.PrettyPrinter.Delaborator.SubExpr.withAppFnArgs {α : Type} {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] (xf : m α) (xa : α → m α) :
m α
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withBindingDomain {α : Type} {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] (x : m α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody {α : Type} {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] [inst : MonadControlT Lean.MetaM m] (n : Lean.Name) (x : m α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withProj {α : Type} [inst : Inhabited α] {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] (x : m α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr {α : Type} [inst : Inhabited α] {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] (x : m α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withLetVarType {α : Type} [inst : Inhabited α] {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] (x : m α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withLetValue {α : Type} [inst : Inhabited α] {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] (x : m α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withLetBody {α : Type} [inst : Inhabited α] {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] [inst : MonadControlT Lean.MetaM m] (x : m α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withNaryFn {α : Type} {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] (x : m α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg {α : Type} {m : Type → Type} [inst : Monad m] [inst : MonadReaderOf Lean.SubExpr m] [inst : MonadWithReaderOf Lean.SubExpr m] (argIdx : Nat) (x : m α) :
m α
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator:
Type
source
instance Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator:
Inhabited Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator
Equations
source
def Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.toPos (iter : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator) :
Lean.SubExpr.Pos
Equations
source
def Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.next (iter : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator) :
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.PrettyPrinter.Delaborator.SubExpr.nextExtraPos {m : Type → Type} [inst : Monad m] [inst : MonadStateOf Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator m] :
m Lean.SubExpr.Pos

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.