Fields.cut.go: def of lawful-fields@0.1.1.0 Import: import lawful-fields@0.1.1.0/fields.bend as Fields Lines 22-35 of lawful-fields@0.1.1.0/fields.bend: https://jend.leeeet.dev/read.txt?path=lawful-fields@0.1.1.0/fields.bend&start_line=22&end_line=35 import Base import lawful-bytes@0.1.1.0/defs.bend as D # n counts the pieces still wanted, this one included; more says the previous # piece ended at a separator; r holds this piece's end. def cut.go(+n: Nat, more: Bool, r: D.Bytes & U32, +to: U32, +sep: U32) -> D.Bytes & List<&2, U32>: match n more: case 0n _: (b, e) = r (b, Nil{}) case 1n+m False{}: (b, e) = r (b, Nil{}) case 1n+m True{}: (b, +e) = r +go = U32.is_lt(e, to) cut.cons(e, cut.go(m, go, cut.next(go && Bool.not(Nat.is_eq(m, 0n)), b, (e + 1 : U32), to, sep), to, sep)) Uses (14): 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=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=Bytes https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=cut.cons https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=cut.next