def set_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pcodec.bend:200

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend as PT

200def set_eq(+xs: List<&2, U32>, +b: U32) -> {PT.set_top(xs, b) == SE.set_msb(xs, b) : List<&2, U32>}:
201  match xs:
202    case Nil{}:
203      {==}
204    case Con{+x, +xt}:
205      match xt:
206        case Nil{}:
207          {==}
208        case Con{+y, +yt}:
209          Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, PT.set_top(Con{y, yt}, b), SE.set_msb(Con{y, yt}, b), set_eq(Con{y, yt}, b))