blob: bfd09acfd3503a8fef392d3998d011be3824f603 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
Require Export Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
Require Import Crypto.Galois.GaloisField.
Module GaloisRep (M: Modulus).
Module G := Galois M.
Module F := GaloisField M.
Import M G F.
Local Open Scope GF_scope.
(* Definition GFSig : ADTSig :=
ADTsignature {
Constructor "FromGF"
: GF -> rep,
Method "ToGF"
: rep -> GF,
Method "Add"
: rep x rep -> rep,
Method "Mult"
: rep x rep -> rep,
Method "Sub"
: rep x rep -> rep,
Method "Div"
: rep x rep -> rep
}. *)
End GaloisRep.
|
