def ef_char

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

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

107# an empty first piece: no single-byte token fits it
108def ef_char(+c: U32, +r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(ds)) == False{} : Bool}:
109  match ds:
110    case Nil{}:
111      {==}
112    case Con{d, t}:
113      ef_char(c, r, t)