@[inline]
Equations
@[inline]
- expr : Lean.Expr
- pos : Lean.PrettyPrinter.Delaborator.Pos
Equations
- Lean.PrettyPrinter.Delaborator.instInhabitedSubExpr = { default := { expr := default, pos := default } }
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.mkRoot e = { expr := e, pos := 1 }
def
Lean.PrettyPrinter.Delaborator.SubExpr.getExpr
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
:
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.getExpr = do let a ← readThe Lean.PrettyPrinter.Delaborator.SubExpr pure a.expr
def
Lean.PrettyPrinter.Delaborator.SubExpr.getPos
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
:
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.getPos = do let a ← readThe Lean.PrettyPrinter.Delaborator.SubExpr pure a.pos
def
Lean.PrettyPrinter.Delaborator.SubExpr.descend
{α : Type}
{m : Type → Type}
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(child : Lean.Expr)
(childIdx : Lean.PrettyPrinter.Delaborator.Pos)
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.descend child childIdx x = withTheReader Lean.PrettyPrinter.Delaborator.SubExpr (fun cfg => { expr := child, pos := cfg.pos * Lean.PrettyPrinter.Delaborator.SubExpr.maxChildren + childIdx }) x
def
Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn
{α : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn x = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr Lean.PrettyPrinter.Delaborator.SubExpr.descend (Lean.Expr.appFn! a) 0 x
def
Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg
{α : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg x = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr Lean.PrettyPrinter.Delaborator.SubExpr.descend (Lean.Expr.appArg! a) 1 x
def
Lean.PrettyPrinter.Delaborator.SubExpr.withType
{α : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadLiftT Lean.MetaM m]
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withType x = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let a ← liftM (Lean.Meta.inferType a) Lean.PrettyPrinter.Delaborator.SubExpr.descend a (Lean.PrettyPrinter.Delaborator.SubExpr.maxChildren - 1) x
partial def
Lean.PrettyPrinter.Delaborator.SubExpr.withAppFnArgs
{α : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(xf : m α)
(xa : α → m α)
:
m α
def
Lean.PrettyPrinter.Delaborator.SubExpr.withBindingDomain
{α : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withBindingDomain x = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr Lean.PrettyPrinter.Delaborator.SubExpr.descend (Lean.Expr.bindingDomain! a) 0 x
def
Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody
{α : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadControlT Lean.MetaM m]
(n : Lean.Name)
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody n x = do let e ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr Lean.Meta.withLocalDecl n (Lean.Expr.binderInfo e) (Lean.Expr.bindingDomain! e) fun fvar => Lean.PrettyPrinter.Delaborator.SubExpr.descend (Lean.Expr.instantiate1 (Lean.Expr.bindingBody! e) fvar) 1 x
def
Lean.PrettyPrinter.Delaborator.SubExpr.withProj
{α : Type}
[inst : Inhabited α]
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withProj x = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.proj x x_1 e x_2 => Lean.PrettyPrinter.Delaborator.SubExpr.descend e 0 x | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.SubExpr" "Lean.PrettyPrinter.Delaborator.SubExpr.withProj" 70 36 "unreachable code has been reached"
def
Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr
{α : Type}
[inst : Inhabited α]
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr x = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.mdata x e x_1 => withTheReader Lean.PrettyPrinter.Delaborator.SubExpr (fun ctx => { expr := e, pos := ctx.pos }) x | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.SubExpr" "Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr" 74 35 "unreachable code has been reached"
def
Lean.PrettyPrinter.Delaborator.SubExpr.withLetVarType
{α : Type}
[inst : Inhabited α]
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withLetVarType x = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.letE x t x_1 x_2 x_3 => Lean.PrettyPrinter.Delaborator.SubExpr.descend t 0 x | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.SubExpr" "Lean.PrettyPrinter.Delaborator.SubExpr.withLetVarType" 78 38 "unreachable code has been reached"
def
Lean.PrettyPrinter.Delaborator.SubExpr.withLetValue
{α : Type}
[inst : Inhabited α]
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withLetValue x = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.letE x x_1 v x_2 x_3 => Lean.PrettyPrinter.Delaborator.SubExpr.descend v 1 x | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.SubExpr" "Lean.PrettyPrinter.Delaborator.SubExpr.withLetValue" 82 38 "unreachable code has been reached"
def
Lean.PrettyPrinter.Delaborator.SubExpr.withLetBody
{α : Type}
[inst : Inhabited α]
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadControlT Lean.MetaM m]
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withLetBody x = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.letE n t v b x => Lean.Meta.withLetDecl n t v fun fvar => let b := Lean.Expr.instantiate1 b fvar; Lean.PrettyPrinter.Delaborator.SubExpr.descend b 2 x | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.SubExpr" "Lean.PrettyPrinter.Delaborator.SubExpr.withLetBody" 86 38 "unreachable code has been reached"
def
Lean.PrettyPrinter.Delaborator.SubExpr.withNaryFn
{α : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withNaryFn x = do let e ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let n : Nat := Lean.Expr.getAppNumArgs e let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getPos let newPos : Lean.PrettyPrinter.Delaborator.Pos := a * Lean.PrettyPrinter.Delaborator.SubExpr.maxChildren ^ n withTheReader Lean.PrettyPrinter.Delaborator.SubExpr (fun cfg => { expr := Lean.Expr.getAppFn e, pos := newPos }) x
def
Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg
{α : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
[inst : MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr m]
(argIdx : Nat)
(x : m α)
:
m α
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg argIdx x = do let e ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let args : Array Lean.Expr := Lean.Expr.getAppArgs e let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getPos let newPos : Lean.PrettyPrinter.Delaborator.Pos := a * Lean.PrettyPrinter.Delaborator.SubExpr.maxChildren ^ (Array.size args - argIdx) + 1 withTheReader Lean.PrettyPrinter.Delaborator.SubExpr (fun cfg => { expr := Array.getOp args argIdx, pos := newPos }) x
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator = { default := { curr := default, top := default } }
def
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.next
(iter : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator)
:
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.next iter = if (iter.curr + 1 == iter.top) = true then { curr := 2 * iter.top, top := Lean.PrettyPrinter.Delaborator.SubExpr.maxChildren * iter.top } else { curr := iter.curr + 1, top := iter.top }
def
Lean.PrettyPrinter.Delaborator.SubExpr.nextExtraPos
{m : Type → Type}
[inst : Monad m]
[inst : MonadStateOf Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator m]
:
Equations
- Lean.PrettyPrinter.Delaborator.SubExpr.nextExtraPos = do let iter ← getThe Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator let pos : Lean.PrettyPrinter.Delaborator.Pos := Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.toPos iter modifyThe Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.next pure pos