inductive MUList.Relation.Rel {α : Type} (s : State.ListST α) (a : State.Actions α) : State.ListST α → Prop

• ModifyData {α : Type} {s : State.ListST α} {a : State.Actions α} (tkn : Tokens.Elem.TId) (d : α) (s' : Tokens.State.Tokens (State.Elemt State.Key α)) : a = State.Actions.ModifyData tkn d → Tokens.State.Tokens.update_data tkn (fun (tkn : State.Elemt State.Key α) => { key := tkn.key, link := tkn.link, data := d }) s = some s' → Rel s a s'
• UnsafeAppend {α : Type} {s : State.ListST α} {a : State.Actions α} (key : State.Key) (data : α) (last : Tokens.Elem.TId) (last_node : State.ListToken α) (s' : State.ListST α) : a = State.Actions.UnsafeAppend key data last → State.ListST.is_last_node last s = true → Tokens.State.Tokens.get last s = some last_node → some s' = State.ListST.upd_link last (some key) (Tokens.State.Tokens.mint (State.serialize_key (some key)) { key := some key, link := none, data := data } s) → Rel s a s'
• UnsafePrepend {α : Type} {s : State.ListST α} {a : State.Actions α} (key : State.Key) (data : α) (root : Tokens.Elem.TId) (root_node : State.ListToken α) (s' : State.ListST α) : a = State.Actions.UnsafePrepend key data root → State.ListST.is_root_node root s = true → Tokens.State.Tokens.get root s = some root_node → some s' = State.ListST.upd_link root (some key) (Tokens.State.Tokens.mint (State.serialize_key (some key)) { key := some key, link := root_node.data.link, data := data } s) → Rel s a s'
• Remove {α : Type} {s : State.ListST α} {a : State.Actions α} (key : State.Key) (rem anchor : Tokens.Elem.TId) (rem_node anchor_node : Tokens.Elem.TokenD (State.Elemt State.Key α)) (s' burnt : State.ListST α) : a = State.Actions.Remove rem anchor → Tokens.State.Tokens.get rem s = some rem_node → rem_node.data.key = some key → Tokens.State.Tokens.get anchor s = some anchor_node → anchor_node.data.link = some key → some burnt = Tokens.State.Tokens.burn rem s → some s' = State.ListST.upd_link anchor rem_node.data.link burnt → Rel s a s'

def MUList.Notation.«term_!_↝_» : Lean.TrailingParserDescr

Equations

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