def remove_absent.list

bend-kit-scheduler@0.4.1.0 · queue_proof.bend:200

import Base
import bend-kit-scheduler@0.4.1.0/queue.bend as Q
import bend-kit-scheduler@0.4.1.0/queue_laws.bend as L

200def remove_absent.list(-A: Data, +xs: List<&2, Q.Ticket<A>>, +i: Nat) -> L.absent.list(A, Q.remove.list(A, xs, i), i):
201  match xs:
202    case Nil{}:
203      Unit{}
204    case Con{t, rest}:
205      +r2 = Q.remove.list(A, rest, i)
206      +er = remove_absent.list(A, rest, i)
207      split(c => L.absent.list(A, Q.remove.list.keep(A, c, t, r2), i), Nat.is_eq(Q.id(A, t), i),
208        e => er,
209        e => L.Both{e, er})