From 81c0f7fe3a2fa418c9f032984354554172a616b4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 17 Nov 2016 14:31:32 -0500 Subject: Update field names in SpecificGen --- src/SpecificGen/GFtemplate3mod4 | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/SpecificGen/GFtemplate3mod4') diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4 index ccee86d1a..d255befeb 100644 --- a/src/SpecificGen/GFtemplate3mod4 +++ b/src/SpecificGen/GFtemplate3mod4 @@ -420,7 +420,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 @@ -446,22 +446,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. -- cgit v1.2.3