Documentation

Lean.Meta.Iterator

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

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

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

      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
        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
          Instances For