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

Equations

• Lean.PrettyPrinter.Delaborator.OptionsPerPos = Lean.RBMap Lean.SubExpr.Pos Lean.Options compare

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

Equations

• Lean.PrettyPrinter.Delaborator.SubExpr.getExpr = do let __do_lift ← readThe Lean.SubExpr pure __do_lift.expr

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

Equations

• Lean.PrettyPrinter.Delaborator.SubExpr.getPos = do let __do_lift ← readThe Lean.SubExpr pure __do_lift.pos

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

Equations

• Lean.PrettyPrinter.Delaborator.SubExpr.descend child childIdx x = withTheReader Lean.SubExpr (fun (cfg : Lean.SubExpr) => { expr := child, pos := Lean.SubExpr.Pos.push cfg.pos childIdx }) x

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

Equations

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

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

Equations

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

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 α

Equations

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

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 α

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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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.

Equations

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

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

Equations

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

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 α

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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 α

Equations

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

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

Equations

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

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 α

Equations

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

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

• curr : Nat
• top : Nat

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

Equations

• Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator = { default := { curr := default, top := default } }

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

Equations

• Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.toPos iter = iter.curr

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.

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.

Equations

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