blob: 02844ea7cc4380170ac653a2e4122471ad0606c0 (
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.AbstractGaloisField.
Module GaloisRep (M: Modulus).
Module G := Galois M.
Module F := AbstractGaloisField 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.
|
