instantiated FqEncoding and FlEncoding (also fixed indentation, which is why the commit looks huge)

1 files changed, 2 insertions, 8 deletions

diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 35fc1d543..a7b8fe987 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -1,3 +1,4 @@
+Require Import Crypto.Spec.Encoding.
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.Spec.CompleteEdwardsCurve.
 
@@ -13,13 +14,6 @@ Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
 
 Coercion Word.wordToNat : Word.word >-> nat.
 
-Class Encoding (T B:Type) := {
-  enc : T -> B ;
-  dec : B -> option T ;
-  encoding_valid : forall x, dec (enc x) = Some x  
-}.
-Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50).
-
 Infix "^" := NPeano.pow.
 Infix "mod" := NPeano.modulo.
 Infix "++" := Word.combine.
@@ -94,4 +88,4 @@ Section EdDSA.
     end
     end
     end%E.
-End EdDSA.
\ No newline at end of file
+End EdDSA.