def carry_con
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as Fieldimport Base
92def carry_con(l: U32, r: Cr) -> Cr:
93 match r:
94 case Cr{a, c}:
95 Cr{Con{l, a}, c}
Uses (3)
Used by (6)
- bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field:carry
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs:cc_con
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs:cl_con
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs:carry_cb
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs:carry_ok
- …