diff options
author | 2016-04-29 18:27:26 -0400 | |
---|---|---|
committer | 2016-04-29 18:27:26 -0400 | |
commit | 728b2f95dc83329c58aef7624283cb945c77b919 (patch) | |
tree | 519e2067b86022405b89287c687977804beacba5 /src/Encoding/PointEncodingPre.v | |
parent | 44c3f52e7d431b4aa5de8e8679155ea2bed9d31c (diff) |
Changed name of Encoding to CanonicalEncoding, and changed notation to match.
Diffstat (limited to 'src/Encoding/PointEncodingPre.v')
-rw-r--r-- | src/Encoding/PointEncodingPre.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v index e023da0ea..73ced869b 100644 --- a/src/Encoding/PointEncodingPre.v +++ b/src/Encoding/PointEncodingPre.v @@ -17,7 +17,7 @@ Section PointEncoding. Context {prm: TwistedEdwardsParams} {sz : nat} {sz_nonzero : (0 < sz)%nat} {bound_check : (Z.to_nat q < 2 ^ sz)%nat} {q_5mod8 : (q mod 8 = 5)%Z} {sqrt_minus1_valid : (@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1} - {FqEncoding : encoding of (F q) as (word sz)} + {FqEncoding : canonical encoding of (F q) as (word sz)} {sign_bit : F q -> bool} {sign_bit_zero : sign_bit 0 = false} {sign_bit_opp : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x)}. Existing Instance prime_q. |