InfoTree utils #
This file contains a few functions that are useful for traversing infotrees.
def
Lean.Elab.InfoTree.visitStateOf
(σ : Type)
{m : Type → Type u_1}
[Monad m]
[MonadStateOf σ m]
(visit : ContextInfo → Info → PersistentArray InfoTree → m Unit)
:
Visit nodes in an infotree, where state is set only within a single branch.
Equations
- Lean.Elab.InfoTree.visitStateOf σ visit = Lean.Elab.InfoTree.visitStateOf.go✝ σ visit none