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
Instances For
partial def
Lean.Elab.InfoTree.visitStateOf.go
{σ : Type}
{m : Type → Type u_1}
[Monad m]
[MonadStateOf σ m]
(visit : ContextInfo → Info → PersistentArray InfoTree → m Unit)
:
Option ContextInfo → InfoTree → m Unit