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.
def
Lean.PrettyPrinter.Delaborator.SubExpr.getExpr
{m : Type → Type}
[Monad m]
[MonadReaderOf Lean.SubExpr m]
:
Instances For
def
Lean.PrettyPrinter.Delaborator.SubExpr.getPos
{m : Type → Type}
[Monad m]
[MonadReaderOf Lean.SubExpr m]
:
Instances For
def
Lean.PrettyPrinter.Delaborator.SubExpr.descend
{α : Type}
{m : Type → Type}
[MonadWithReaderOf Lean.SubExpr m]
(child : Lean.Expr)
(childIdx : Nat)
(x : m α)
:
m α
Instances For
def
Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn
{α : Type}
{m : Type → Type}
[Monad m]
[MonadReaderOf Lean.SubExpr m]
[MonadWithReaderOf Lean.SubExpr m]
(x : m α)
:
m α
Instances For
def
Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg
{α : Type}
{m : Type → Type}
[Monad m]
[MonadReaderOf Lean.SubExpr m]
[MonadWithReaderOf Lean.SubExpr m]
(x : m α)
:
m α
Instances For
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 α
Instances For
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 α
Instances For
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 α
Instances For
def
Lean.PrettyPrinter.Delaborator.SubExpr.withProj
{α : Type}
[Inhabited α]
{m : Type → Type}
[Monad m]
[MonadReaderOf Lean.SubExpr m]
[MonadWithReaderOf Lean.SubExpr m]
(x : m α)
:
m α
Instances For
def
Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr
{α : Type}
[Inhabited α]
{m : Type → Type}
[Monad m]
[MonadReaderOf Lean.SubExpr m]
[MonadWithReaderOf Lean.SubExpr m]
(x : m α)
:
m α
Instances For
def
Lean.PrettyPrinter.Delaborator.SubExpr.withLetVarType
{α : Type}
[Inhabited α]
{m : Type → Type}
[Monad m]
[MonadReaderOf Lean.SubExpr m]
[MonadWithReaderOf Lean.SubExpr m]
(x : m α)
:
m α
Instances For
def
Lean.PrettyPrinter.Delaborator.SubExpr.withLetValue
{α : Type}
[Inhabited α]
{m : Type → Type}
[Monad m]
[MonadReaderOf Lean.SubExpr m]
[MonadWithReaderOf Lean.SubExpr m]
(x : m α)
:
m α
Instances For
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 α
Instances For
def
Lean.PrettyPrinter.Delaborator.SubExpr.withNaryFn
{α : Type}
{m : Type → Type}
[Monad m]
[MonadReaderOf Lean.SubExpr m]
[MonadWithReaderOf Lean.SubExpr m]
(x : m α)
:
m α
Instances For
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 α
Instances For
Instances For
def
Lean.PrettyPrinter.Delaborator.SubExpr.nextExtraPos
{m : Type → Type}
[Monad m]
[MonadStateOf Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator m]
:
The positioning scheme guarantees that there will be an infinite number of extra positions
which are never used by Expr
s. The HoleIterator
always points at the next such "hole".
We use these to attach additional Elab.Info
.