Commit 2025-11-21 23:43 5a2faa09

View on Github →

feat: InfoTree API: InfoTree.findSome(M)? and InfoTree.onHighestNode? (#31725) This PR adds the following basic InfoTree API:

def findSome? {α} (f : ContextInfo → Info → PersistentArray InfoTree → Option α)
    (t : InfoTree) (ctx? : Option ContextInfo := none) : Option α
def findSomeM? {m : Type → Type} [Monad m] {α}
    (f : ContextInfo → Info → PersistentArray InfoTree → m (Option α))
    (t : InfoTree) (ctx? : Option ContextInfo := none) : m (Option α)
def onHighestNode? {α} (t : InfoTree) (ctx? : Option ContextInfo)
    (f : ContextInfo → Info → PersistentArray InfoTree → α) : Option α

Note that onHighestNode? has an explicit Option ContextInfo argument. This is because onHighestNode? is more likely to be called in the middle of a larger traversal, during which it is essential to pass the surrounding ContextInfo. Making this argument explicit mitigates the increased risk of a footgun here. This functionality is motivated by use in other PRs.

Estimated changes