structure Lean.Meta.Iterator (α : Type) : Type

Provides an interface for iterating over values that are bundled with the Meta state they are valid in.

• next : MetaM (Option (α × SavedState))

  Function for getting next value and state pair.

def Lean.Meta.Iterator.ofList {α : Type} (l : List α) : MetaM (Meta.Iterator α)

Convert a list into an iterator with the current state.

def Lean.Meta.Iterator.filterMapM {α β : Type} (f : α → MetaM (Option β)) (L : Meta.Iterator α) : Meta.Iterator β

Map and filter results of iterator and returning only those values returned by f.

def Lean.Meta.Iterator.head {α : Type} (L : Meta.Iterator α) : MetaM α

Find the first value in the iterator while resetting state or call failure if empty.

def Lean.Meta.Iterator.firstM {α β : Type} (L : Meta.Iterator α) (f : α → MetaM (Option β)) : MetaM β

Return the first value returned by the iterator that f succeeds on.