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, reducible]

abbrev Lean.PrettyPrinter.Delaborator.OptionsPerPos : Type

def Lean.PrettyPrinter.Delaborator.SubExpr.getExpr {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] : m Lean.Expr

def Lean.PrettyPrinter.Delaborator.SubExpr.getPos {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] : m Lean.SubExpr.Pos

def Lean.PrettyPrinter.Delaborator.SubExpr.descend {α : Type} {m : Type → Type} [MonadWithReaderOf Lean.SubExpr m] (child : Lean.Expr) (childIdx : Nat) (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withType {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] [MonadLiftT Lean.MetaM m] (x : m α) : m α

partial def Lean.PrettyPrinter.Delaborator.SubExpr.withAppFnArgs {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (xf : m α) (xa : α → m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withBindingDomain {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] [MonadControlT Lean.MetaM m] (n : Lake.Name) (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withProj {α : Type} [Inhabited α] {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr {α : Type} [Inhabited α] {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withLetVarType {α : Type} [Inhabited α] {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withLetValue {α : Type} [Inhabited α] {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withLetBody {α : Type} [Inhabited α] {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] [MonadControlT Lean.MetaM m] (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withNaryFn {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (x : m α) : m α

def Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] (argIdx : Nat) (x : m α) : m α

structure Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator : Type

• curr : Nat
• top : Nat

instance Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator : Inhabited Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator

def Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.toPos (iter : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator) : Lean.SubExpr.Pos

def Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.next (iter : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator) : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator

def Lean.PrettyPrinter.Delaborator.SubExpr.nextExtraPos {m : Type → Type} [Monad m] [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.