diff options
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index f4afcb935..9bd3cac5e 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -9,12 +9,11 @@ Require Export Crypto.Util.FixCoqMistakes. Module Import ModuloCoq8485. Import NPeano Nat. - Infix "mod" := modulo (at level 40, no associativity). + Infix "mod" := modulo. End ModuloCoq8485. Notation is_eq_dec := (DecidableRel _) (only parsing). -Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop)) - (at level 10, T at level 8, R at level 8, only parsing). +Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop)) (only parsing). Notation eq_dec x y := (@dec (_ x y) _) (only parsing). Notation "x =? y" := (eq_dec x y) : type_scope. @@ -305,7 +304,7 @@ Module Group. Lemma surjective_homomorphism_from_group {G EQ OP ID INV} {groupG:@group G EQ OP ID INV} {H eq op id inv} - {Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y}} + {Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y} } {Proper_op:Proper(eq==>eq==>eq)op} {Proper_inv:Proper(eq==>eq)inv} {phi iph} {Proper_phi:Proper(EQ==>eq)phi} {Proper_iph:Proper(eq==>EQ)iph} @@ -330,7 +329,7 @@ Module Group. Lemma isomorphism_to_subgroup_group {G EQ OP ID INV} - {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}} + {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} } {Proper_OP:Proper(EQ==>EQ==>EQ)OP} {Proper_INV:Proper(EQ==>EQ)INV} {H eq op id inv} {groupG:@group H eq op id inv} @@ -534,7 +533,7 @@ Module Ring. Lemma isomorphism_to_subring_ring {T EQ ZERO ONE OPP ADD SUB MUL} - {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}} + {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} } {Proper_OPP:Proper(EQ==>EQ)OPP} {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD} {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB} @@ -664,7 +663,7 @@ Module Field. Lemma isomorphism_to_subfield_field {T EQ ZERO ONE OPP ADD SUB MUL INV DIV} - {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}} + {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} } {Proper_OPP:Proper(EQ==>EQ)OPP} {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD} {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB} |