PROOF.bits.nany_meets: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3083-3097 of bend-osdev-apparmor@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&start_line=3083&end_line=3097

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

# a request with no bit set meets nothing
def 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}:
  match r:
    case Nil{}:
      {==}
    case Con{z, zs}:
      match z:
        case True{}:
          {==}
        case False{}:
          match d:
            case Nil{}:
              b.and_false_r(Bool.not(P.AaBits.any(zs)))
            case Con{y, ys}:
              bits.nany_meets(zs, ys)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.and_false_r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaBits.any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaBits.meets