def from_app

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:3486

import Base
import bend-osdev-apparmor@0.1.0.0/perm.bend as P
import bend-osdev-apparmor@0.1.0.0/eval.bend as V

3486def from_app(+xs: List<&2, P.AaGrant>, +ys: List<&2, P.AaGrant>, +acc: V.AaAcc) -> {V.AaAcc.from(P.AaGrant.append(xs, ys), acc) == V.AaAcc.from(ys, V.AaAcc.from(xs, acc)) : V.AaAcc}:
3487  match xs:
3488    case Nil{}:
3489      {==}
3490    case Con{g, t}:
3491      from_app(t, ys, V.AaAcc.add(acc, g))