Documentation

Lean.Util.MonadBacktrack

Similar to MonadState, but it retrieves/restores only the "backtrackable" part of the state

  • saveState : m s
  • restoreState : sm Unit
Instances
    def Lean.commitWhenSome? {m : TypeType} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x? : m (Option α)) :
    m (Option α)

    Execute x?, but backtrack state if result is none or an exception was thrown.

    Equations
      Instances For
        def Lean.commitWhenSomeNoEx? {m : TypeType} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x? : m (Option α)) :
        m (Option α)

        Execute x?, but backtrack state if result is none or an exception was thrown. If an exception is thrown, none is returned. That is, this function is similar to commitWhenSome?, but swallows the exception and returns none.

        Equations
          Instances For
            def Lean.commitWhen {m : TypeType} {s : Type} {ε : Type u_1} [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x : m Bool) :
            Equations
              Instances For
                def Lean.commitIfNoEx {m : TypeType} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x : m α) :
                m α
                Equations
                  Instances For
                    def Lean.withoutModifyingState {m : TypeType} {s α : Type} [Monad m] [MonadFinally m] [MonadBacktrack s m] (x : m α) :
                    m α
                    Equations
                      Instances For
                        def Lean.observing? {m : TypeType} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x : m α) :
                        m (Option α)
                        Equations
                          Instances For
                            Equations