def ceq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/cong.bend:10

import Base

10def ceq(+pp: Nat, +a: Nat, +b: Nat) -> Data:
11  {Nat.mod(a, 1n+pp) == Nat.mod(b, 1n+pp) : Nat}