theorem MOList.Computational.ComputationalRelation {α : Type} {a : State.Actions α} {s s' : MUList.State.ListST α} : Computation.next a s = ComputationResult.Success s' ↔ Relation.Rel s a s'

def MOList.Computational.runActions {α : Type} (acc : MUList.State.ListST α) (ls : List (State.Actions α)) : ComputationResult Computation.Err (MUList.State.ListST α)

Equations

• MOList.Computational.runActions acc [] = success acc
• MOList.Computational.runActions acc (c :: cs) = do let x ← MOList.Computation.next c acc MOList.Computational.runActions x cs