def lred

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fprot.bend:122

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L

122def lred(+c: List<&2, Nat>, +k: Nat, xs: List<&2, Nat>) -> {L.reduce(c, k, xs) == L.reduce_go(c, k, xs) : List<&2, Nat>}:
123  match xs:
124    case Nil{}:
125      {==}
126    case x <> t:
127      {==}