def bits.nany_meets

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

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

3083# a request with no bit set meets nothing
3084def bits.nany_meets(+r: List<&2, Bool>, +d: List<&2, Bool>) -> {Bool.and(Bool.not(P.AaBits.any(r)), P.AaBits.meets(r, d)) == False{} : Bool}:
3085  match r:
3086    case Nil{}:
3087      {==}
3088    case Con{z, zs}:
3089      match z:
3090        case True{}:
3091          {==}
3092        case False{}:
3093          match d:
3094            case Nil{}:
3095              b.and_false_r(Bool.not(P.AaBits.any(zs)))
3096            case Con{y, ys}:
3097              bits.nany_meets(zs, ys)