def b_cg

bendtorch@1.3.0.0 · PROOF.bend:635

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

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