diff options
Diffstat (limited to 'src/SpecificGen/GFtemplate5mod8')
| -rw-r--r-- | src/SpecificGen/GFtemplate5mod8 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/SpecificGen/GFtemplate5mod8 b/src/SpecificGen/GFtemplate5mod8 index c5d0d1cfe..008010efd 100644 --- a/src/SpecificGen/GFtemplate5mod8 +++ b/src/SpecificGen/GFtemplate5mod8 @@ -428,7 +428,7 @@ Proof. { intros; apply encode_rep. } Qed. -Definition field{{{k}}}{{{c}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. +Definition field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. Lemma carry_field_and_homomorphisms : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div @@ -454,22 +454,22 @@ Proof. { intros; apply encode_rep. } Qed. -Definition carry_field : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. +Definition carry_field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. -Lemma homomorphism_F_encode +Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_encode : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul encode. Proof. apply field_and_homomorphisms. Qed. -Lemma homomorphism_F_decode +Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_decode : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply field_and_homomorphisms. Qed. -Lemma homomorphism_carry_F_encode +Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_encode : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul encode. Proof. apply carry_field_and_homomorphisms. Qed. -Lemma homomorphism_carry_F_decode +Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_decode : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply carry_field_and_homomorphisms. Qed. |