src/Rep/ECRep.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16


Require Export Crypto.Galois.GaloisField.

Module ECRep (M: Modulus).
  Module F := GaloisField M.
  Import F.
  Local Open Scope GF_scope.

  (* Definition ECSig : ADTSig :=
    ADTsignature {
        Constructor "FromTwistedXY"
               : GF x GF -> rep,
        Method "Add"
               : rep x rep -> rep,
      }.*)
End ECRep.