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

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

• next : Lean.MetaM (Option (α × Lean.Meta.SavedState))

  Function for getting next value and state pair.

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

Convert a list into an iterator with the current state.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.Meta.Iterator.filterMapM f L = { next := Lean.Meta.Iterator.filterMapM._next f L }

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

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

Equations

• Lean.Meta.Iterator.head L = do let __do_lift ← L.next match __do_lift with | none => failure | some (x, s) => do Lean.restoreState s pure x

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

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

Equations

• Lean.Meta.Iterator.firstM L f = Lean.Meta.Iterator.head (Lean.Meta.Iterator.filterMapM f L)