def gr_star2

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

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

197# ... a double star takes any h
198def gr_star2(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, ds)) == G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, ds) : Bool}:
199  match ds:
200    case Nil{}:
201      {==}
202    case Con{d, t}:
203      match d:
204        case Nil{}:
205          gr_star2(r, h, t)
206        case Con{p, ps}:
207          %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, t)), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, t), gr_star2(r, h, t)) : {Bool.or(G.AaGSeq.fits(r, ps), _) == Bool.or(G.AaGSeq.fits(r, ps), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, t)) : Bool}
208          {==}