PROOF.gr_class: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 172-182 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=172&end_line=182

import Base
import bend-osdev-apparmor@0.1.0.0/text.bend as X
import bend-osdev-apparmor@0.1.0.0/glob.bend as G

def gr_class(+n: Bool, +rs: List<&2, G.AaGRange>, +r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, ds)) : Bool}:
  match ds:
    case Nil{}:
      Equal.sym(Bool, Bool.and(G.AaGClass.has(n, rs, h), False{}), False{}, b.and_false_r(G.AaGClass.has(n, rs, h)))
    case Con{d, t}:
      match d:
        case Nil{}:
          gr_class(n, rs, r, h, t)
        case Con{p, ps}:
          %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, t)), Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, t)), gr_class(n, rs, r, h, t)) : {Bool.or(Bool.and(Bool.and(G.AaGClass.has(n, rs, h), X.AaText.is_nil(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(G.AaGClass.has(n, rs, h), Bool.or(Bool.and(X.AaText.is_nil(p), G.AaGSeq.fits(r, ps)), fe_any(r, t))) : Bool}
          b.factor(G.AaGClass.has(n, rs, h), X.AaText.is_nil(p), G.AaGSeq.fits(r, ps), fe_any(r, t))

Uses (16):
  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.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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/PROOF.bend&name=b.factor
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGClass.has
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGCuts.grow
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGRange
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGSeq.fits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGSeq.fits_any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGTok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/text.bend&name=AaText.is_nil