def cg

bendtorch@1.3.0.0 · PROOF.bend:360

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

360def cg(k: Nat, xs: List<&1, T.FS>, acc: List<&1, T.FS>) -> CGR<k, xs, acc>:
361  match k xs:
362    case 1n+m Con{x, t}:
363      cg_con(m, x, t, acc, cg(m, t, x <> acc))
364    case 0n ys:
365      cg_base(0n, ys, acc, {==}, go_app(acc, Nil{}, ys))
366    case 1n+m Nil{}:
367      cg_base(1n+m, Nil{}, acc, {==}, go_app(acc, Nil{}, Nil{}))