PROOF.b_cg: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/PROOF.bend as PROOF
Lines 635-642 of bendtorch@1.3.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/PROOF.bend&start_line=635&end_line=642

import Base
import bendtorch@1.3.0.0/main.bend as T

def b_cg(k: Nat, xs: List<&1, T.BG>, acc: List<&1, T.BG>) -> b_CGR<k, xs, acc>:
  match k xs:
    case 1n+m Con{x, t}:
      b_cg_con(m, x, t, acc, b_cg(m, t, x <> acc))
    case 0n ys:
      b_cg_base(0n, ys, acc, {==}, b_go_app(acc, Nil{}, ys))
    case 1n+m Nil{}:
      b_cg_base(1n+m, Nil{}, acc, {==}, b_go_app(acc, Nil{}, Nil{}))

Uses (7):
  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=bendtorch@1.3.0.0/PROOF.bend&name=b_CGR
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_cg_base
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_cg_con
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_go_app
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=BG