def Freeze.value

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/curve25519/field.bend:152

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F

152# the canonical representative, which is the 32-byte encoding
153def Freeze.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
154  {value(F.freeze(a)) == Nat.mod(value(a), prime(one)) : Nat}