ProofCut.CG: def of lawful-fields@0.1.1.0
Import: import lawful-fields@0.1.1.0/proof_cut.bend as ProofCut
Lines 644-652 of lawful-fields@0.1.1.0/proof_cut.bend: https://jend.leeeet.dev/read.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&start_line=644&end_line=652

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

def CG(+n: Nat, more: Bool, +e: U32, +len: U32, +t: P.Tree<U32>, +to: U32, +sep: U32) -> List<&2, U32>:
  match n more:
    case 0n _:
      Nil{}
    case 1n+m False{}:
      Nil{}
    case 1n+m True{}:
      +go = U32.is_lt(e, to)
      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)}

Uses (11):
  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=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-arrays@0.1.0.0/proof_tree.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=NX