def CG

lawful-fields@0.1.1.0 · proof_cut.bend:644

import Base
import lawful-arrays@0.1.0.0/proof_tree.bend as P

644def CG(+n: Nat, more: Bool, +e: U32, +len: U32, +t: P.Tree<U32>, +to: U32, +sep: U32) -> List<&2, U32>:
645  match n more:
646    case 0n _:
647      Nil{}
648    case 1n+m False{}:
649      Nil{}
650    case 1n+m True{}:
651      +go = U32.is_lt(e, to)
652      Con{e, CG(m, go, NX(go && Bool.not(Nat.is_eq(m, 0n)), len, t, (e + 1 : U32), to, sep), len, t, to, sep)}