def r_o

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

76def r_o(+pp: Nat, +x: List<&2, U32>, +a: Nat, +r: R(pp, x, a)) -> {LM.okb(32n, x, 255n) == True{} : Bool}:
77  match r:
78    case (o, c):
79      o