Pcodec.r_one: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as Pcodec
Lines 54-55 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&start_line=54&end_line=55

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

def r_one(+pp: Nat) -> RL.R(pp, F.one(), 1n):
  ({==}, G.c_refl(pp, 1n))

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&name=c_refl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=R
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=one