def r_c

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/rel.bend:81

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G

81def r_c(+pp: Nat, +x: List<&2, U32>, +a: Nat, +r: R(pp, x, a)) -> G.ceq(pp, FS.value(x), a):
82  match r:
83    case (o, c):
84      c