Documentation

Lean.Util.MonadBacktrack

  • saveState : m s✝
  • restoreState : s✝m Unit

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

Instances
    def Lean.commitWhenSome? {m : TypeType} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [Lean.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
    • One or more equations did not get rendered due to their size.
    Instances For
      def Lean.commitWhenSomeNoEx? {m : TypeType} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [Lean.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
      • One or more equations did not get rendered due to their size.
      Instances For
        def Lean.commitWhen {m : TypeType} {s : Type} {ε : Type u_1} [Monad m] [Lean.MonadBacktrack s m] [MonadExcept ε m] (x : m Bool) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Lean.commitIfNoEx {m : TypeType} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [Lean.MonadBacktrack s m] [MonadExcept ε m] (x : m α) :
          m α
          Equations
          Instances For
            def Lean.withoutModifyingState {m : TypeType} {s : Type} {α : Type} [Monad m] [MonadFinally m] [Lean.MonadBacktrack s m] (x : m α) :
            m α
            Equations
            Instances For
              def Lean.observing? {m : TypeType} {s : Type} {ε : Type u_1} {α : Type} [Monad m] [Lean.MonadBacktrack s m] [MonadExcept ε m] (x : m α) :
              m (Option α)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations