def r_one
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pcodec.bend:54
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as Pcodec
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL
54def r_one(+pp: Nat) -> RL.R(pp, F.one(), 1n):
55 ({==}, G.c_refl(pp, 1n))