Provides an interface 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.
Instances For
Convert a list into an iterator with the current state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Meta.Iterator.filterMapM
{α β : Type}
(f : α → Lean.MetaM (Option β))
(L : Lean.Meta.Iterator α)
:
Map and filter results of iterator and returning only those values returned
by f
.
Instances For
Find the first value in the iterator while resetting state or call failure
if empty.
Equations
- L.head = do let __do_lift ← L.next match __do_lift with | none => failure | some (x, s) => do Lean.restoreState s pure x
Instances For
def
Lean.Meta.Iterator.firstM
{α β : Type}
(L : Lean.Meta.Iterator α)
(f : α → Lean.MetaM (Option β))
:
Return the first value returned by the iterator that f
succeeds on.
Equations
- L.firstM f = (Lean.Meta.Iterator.filterMapM f L).head