def MOList.Utils.find_token_next_less_cand {α : Type} (ls : MUList.State.ListST α) (c : MUList.State.ListToken α) (ck : MUList.State.Key) (corr : c.data.key = some ck) (k : MUList.State.Key) : MUList.State.ListToken α

Equations

• One or more equations did not get rendered due to their size.
• MOList.Utils.find_token_next_less_cand [] c ck corr k = c
• MOList.Utils.find_token_next_less_cand (none :: rs) c ck corr k = MOList.Utils.find_token_next_less_cand rs c ck corr k

def MOList.Utils.find_token_next_less {α : Type} (ls : MUList.State.ListST α) (k : MUList.State.Key) : Option (MUList.State.ListToken α)

Equations

• One or more equations did not get rendered due to their size.
• MOList.Utils.find_token_next_less [] k = none
• MOList.Utils.find_token_next_less (none :: rs) k = MOList.Utils.find_token_next_less rs k