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.

@[reducible, inline]

abbrev Lean.PrettyPrinter.Delaborator.OptionsPerPos : Type

def Lean.PrettyPrinter.Delaborator.OptionsPerPos.insertAt (optionsPerPos : OptionsPerPos) (pos : SubExpr.Pos) (name : Name) (value : DataValue) : OptionsPerPos

def Lean.PrettyPrinter.Delaborator.OptionsPerPos.merge : OptionsPerPos → OptionsPerPos → OptionsPerPos

Merges two collections of options, where the second overrides the first.

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

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

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

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

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

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

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

Uses xa to compute the fold across the arguments of an application, where xf provides the initial value and is evaluated in the context of the head of the application.

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

Uses xa to compute the fold across up to maxArgs outermost arguments of an application, where xf provides the initial value and is evaluated in the context of the application minus the arguments being folded across.

def Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFn {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (maxArgs : Nat) (xf : m α) : m α

Runs xf in the context of Lean.Expr.getBoundedAppFn maxArgs. This is equivalent to withBoundedAppFnArgs maxArgs xf pure.

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

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

Assumes the SubExpr is a lambda or forall.

1. Creates a local declaration for this binder using the name n.
2. Evaluates v using the fvar for the local declaration.
3. Enters the binding body, and evaluates x using this result.

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

Assumes the SubExpr is a lambda or forall. Creates a local declaration for this binder using the name n, enters the binding body, and evaluates x.

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

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

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

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

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

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

def Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf 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 HoleIterator

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

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

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

Note: these positions are incompatible with Lean.SubExpr.Pos.push since the iterator will eventually yield every child of every returned position.