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
      Instances For
        def Lean.Meta.Iterator.filterMapM {α β : Type} (f : αMetaM (Option β)) (L : Meta.Iterator α) :

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

        Equations
          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 : Meta.Iterator α) (f : αMetaM (Option β)) :

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

                Equations
                  Instances For