inductive MUList.Computation.Err : Type

• NonExistentKey : State.Key → Err
• RemEmptyKey : Err
• NonExistentTkn : Tokens.Elem.TId → Err
• NotLast : Tokens.Elem.TId → Err
• NotRoot : Tokens.Elem.TId → Err
• NotMember : State.Key → Tokens.Elem.TId → Err
• NotPrevious : Tokens.Elem.TId → State.Key → Err

instance MUList.Computation.instReprErr : Repr Err

Equations

• MUList.Computation.instReprErr = { reprPrec := MUList.Computation.instReprErr.repr }

def MUList.Computation.instReprErr.repr : Err → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance MUList.Computation.instToStringErr : ToString Err

Equations

• One or more equations did not get rendered due to their size.

def MUList.Computation.find_token {α : Type} (s : State.ListST α) (tid : Tokens.Elem.TId) : ComputationResult Err (State.ListToken α)

Equations

• MUList.Computation.find_token s tid = fromOptionWith (Tokens.State.Tokens.get tid s) (MUList.Computation.Err.NonExistentTkn tid)

theorem MUList.Computation.find_token_find {α : Type} {tid : Tokens.Elem.TId} {nd : State.ListToken α} {s : State.ListST α} (H : find_token s tid = ComputationResult.Success nd) : Tokens.State.Tokens.get tid s = some nd

theorem MUList.Computation.find_token_find' {α : Type} {tid : Tokens.Elem.TId} {nd : Tokens.Elem.TokenD (State.Elemt State.Key α)} {s : State.ListST α} (H : Tokens.State.Tokens.get tid s = some nd) : find_token s tid = ComputationResult.Success nd

theorem MUList.Computation.find_token_get {α β : Type} {tid : Tokens.Elem.TId} {nd : Tokens.Elem.TokenD (State.Elemt State.Key α)} {s : State.ListST α} (f : α → β) (H : Tokens.State.Tokens.get tid s = some nd) : State.ListST.get_data tid f s = some (f nd.data.data)

def MUList.Computation.next {α : Type} (a : State.Actions α) (s : State.ListST α) : ComputationResult Err (State.ListST α)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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