diff options
Diffstat (limited to 'theories/ZArith/BinInt.v')
-rw-r--r-- | theories/ZArith/BinInt.v | 162 |
1 files changed, 81 insertions, 81 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index f3f7b850e..0f709d686 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1375,87 +1375,87 @@ Infix ">?" := Z.gtb (at level 70, no associativity) : Z_scope. (** Compatibility Notations *) -Notation Zdouble_plus_one := Z.succ_double (only parsing). -Notation Zdouble_minus_one := Z.pred_double (only parsing). -Notation Zdouble := Z.double (only parsing). -Notation ZPminus := Z.pos_sub (only parsing). -Notation Zsucc' := Z.succ (only parsing). -Notation Zpred' := Z.pred (only parsing). -Notation Zplus' := Z.add (only parsing). -Notation Zplus := Z.add (only parsing). (* Slightly incompatible *) -Notation Zopp := Z.opp (only parsing). -Notation Zsucc := Z.succ (only parsing). -Notation Zpred := Z.pred (only parsing). -Notation Zminus := Z.sub (only parsing). -Notation Zmult := Z.mul (only parsing). -Notation Zcompare := Z.compare (only parsing). -Notation Zsgn := Z.sgn (only parsing). -Notation Zle := Z.le (only parsing). -Notation Zge := Z.ge (only parsing). -Notation Zlt := Z.lt (only parsing). -Notation Zgt := Z.gt (only parsing). -Notation Zmax := Z.max (only parsing). -Notation Zmin := Z.min (only parsing). -Notation Zabs := Z.abs (only parsing). -Notation Zabs_nat := Z.abs_nat (only parsing). -Notation Zabs_N := Z.abs_N (only parsing). -Notation Z_of_nat := Z.of_nat (only parsing). -Notation Z_of_N := Z.of_N (only parsing). - -Notation Zind := Z.peano_ind (only parsing). -Notation Zopp_0 := Z.opp_0 (only parsing). -Notation Zopp_neg := Z.opp_Zneg (only parsing). -Notation Zopp_involutive := Z.opp_involutive (only parsing). -Notation Zopp_inj := Z.opp_inj (only parsing). -Notation Zplus_0_l := Z.add_0_l (only parsing). -Notation Zplus_0_r := Z.add_0_r (only parsing). -Notation Zplus_comm := Z.add_comm (only parsing). -Notation Zopp_plus_distr := Z.opp_add_distr (only parsing). -Notation Zopp_succ := Z.opp_succ (only parsing). -Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing). -Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing). -Notation Zplus_assoc := Z.add_assoc (only parsing). -Notation Zplus_permute := Z.add_shuffle3 (only parsing). -Notation Zplus_reg_l := Z.add_reg_l (only parsing). -Notation Zplus_succ_l := Z.add_succ_l (only parsing). -Notation Zplus_succ_comm := Z.add_succ_comm (only parsing). -Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing). -Notation Zsucc_inj := Z.succ_inj (only parsing). -Notation Zsucc'_inj := Z.succ_inj (only parsing). -Notation Zsucc'_pred' := Z.succ_pred (only parsing). -Notation Zpred'_succ' := Z.pred_succ (only parsing). -Notation Zpred'_inj := Z.pred_inj (only parsing). -Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing). -Notation Zminus_0_r := Z.sub_0_r (only parsing). -Notation Zminus_diag := Z.sub_diag (only parsing). -Notation Zminus_plus_distr := Z.sub_add_distr (only parsing). -Notation Zminus_succ_r := Z.sub_succ_r (only parsing). -Notation Zminus_plus := Z.add_simpl_l (only parsing). -Notation Zmult_0_l := Z.mul_0_l (only parsing). -Notation Zmult_0_r := Z.mul_0_r (only parsing). -Notation Zmult_1_l := Z.mul_1_l (only parsing). -Notation Zmult_1_r := Z.mul_1_r (only parsing). -Notation Zmult_comm := Z.mul_comm (only parsing). -Notation Zmult_assoc := Z.mul_assoc (only parsing). -Notation Zmult_permute := Z.mul_shuffle3 (only parsing). -Notation Zmult_1_inversion_l := Z.mul_eq_1 (only parsing). -Notation Zdouble_mult := Z.double_spec (only parsing). -Notation Zdouble_plus_one_mult := Z.succ_double_spec (only parsing). -Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (only parsing). -Notation Zmult_opp_opp := Z.mul_opp_opp (only parsing). -Notation Zmult_opp_comm := Z.mul_opp_comm (only parsing). -Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (only parsing). -Notation Zmult_plus_distr_r := Z.mul_add_distr_l (only parsing). -Notation Zmult_plus_distr_l := Z.mul_add_distr_r (only parsing). -Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (only parsing). -Notation Zmult_reg_l := Z.mul_reg_l (only parsing). -Notation Zmult_reg_r := Z.mul_reg_r (only parsing). -Notation Zmult_succ_l := Z.mul_succ_l (only parsing). -Notation Zmult_succ_r := Z.mul_succ_r (only parsing). -Notation Zpos_xI := Z.pos_xI (only parsing). -Notation Zpos_xO := Z.pos_xO (only parsing). -Notation Zneg_xI := Z.neg_xI (only parsing). -Notation Zneg_xO := Z.neg_xO (only parsing). +Notation Zdouble_plus_one := Z.succ_double (compat "8.3"). +Notation Zdouble_minus_one := Z.pred_double (compat "8.3"). +Notation Zdouble := Z.double (compat "8.3"). +Notation ZPminus := Z.pos_sub (compat "8.3"). +Notation Zsucc' := Z.succ (compat "8.3"). +Notation Zpred' := Z.pred (compat "8.3"). +Notation Zplus' := Z.add (compat "8.3"). +Notation Zplus := Z.add (compat "8.3"). (* Slightly incompatible *) +Notation Zopp := Z.opp (compat "8.3"). +Notation Zsucc := Z.succ (compat "8.3"). +Notation Zpred := Z.pred (compat "8.3"). +Notation Zminus := Z.sub (compat "8.3"). +Notation Zmult := Z.mul (compat "8.3"). +Notation Zcompare := Z.compare (compat "8.3"). +Notation Zsgn := Z.sgn (compat "8.3"). +Notation Zle := Z.le (compat "8.3"). +Notation Zge := Z.ge (compat "8.3"). +Notation Zlt := Z.lt (compat "8.3"). +Notation Zgt := Z.gt (compat "8.3"). +Notation Zmax := Z.max (compat "8.3"). +Notation Zmin := Z.min (compat "8.3"). +Notation Zabs := Z.abs (compat "8.3"). +Notation Zabs_nat := Z.abs_nat (compat "8.3"). +Notation Zabs_N := Z.abs_N (compat "8.3"). +Notation Z_of_nat := Z.of_nat (compat "8.3"). +Notation Z_of_N := Z.of_N (compat "8.3"). + +Notation Zind := Z.peano_ind (compat "8.3"). +Notation Zopp_0 := Z.opp_0 (compat "8.3"). +Notation Zopp_neg := Z.opp_Zneg (compat "8.3"). +Notation Zopp_involutive := Z.opp_involutive (compat "8.3"). +Notation Zopp_inj := Z.opp_inj (compat "8.3"). +Notation Zplus_0_l := Z.add_0_l (compat "8.3"). +Notation Zplus_0_r := Z.add_0_r (compat "8.3"). +Notation Zplus_comm := Z.add_comm (compat "8.3"). +Notation Zopp_plus_distr := Z.opp_add_distr (compat "8.3"). +Notation Zopp_succ := Z.opp_succ (compat "8.3"). +Notation Zplus_opp_r := Z.add_opp_diag_r (compat "8.3"). +Notation Zplus_opp_l := Z.add_opp_diag_l (compat "8.3"). +Notation Zplus_assoc := Z.add_assoc (compat "8.3"). +Notation Zplus_permute := Z.add_shuffle3 (compat "8.3"). +Notation Zplus_reg_l := Z.add_reg_l (compat "8.3"). +Notation Zplus_succ_l := Z.add_succ_l (compat "8.3"). +Notation Zplus_succ_comm := Z.add_succ_comm (compat "8.3"). +Notation Zsucc_discr := Z.neq_succ_diag_r (compat "8.3"). +Notation Zsucc_inj := Z.succ_inj (compat "8.3"). +Notation Zsucc'_inj := Z.succ_inj (compat "8.3"). +Notation Zsucc'_pred' := Z.succ_pred (compat "8.3"). +Notation Zpred'_succ' := Z.pred_succ (compat "8.3"). +Notation Zpred'_inj := Z.pred_inj (compat "8.3"). +Notation Zsucc'_discr := Z.neq_succ_diag_r (compat "8.3"). +Notation Zminus_0_r := Z.sub_0_r (compat "8.3"). +Notation Zminus_diag := Z.sub_diag (compat "8.3"). +Notation Zminus_plus_distr := Z.sub_add_distr (compat "8.3"). +Notation Zminus_succ_r := Z.sub_succ_r (compat "8.3"). +Notation Zminus_plus := Z.add_simpl_l (compat "8.3"). +Notation Zmult_0_l := Z.mul_0_l (compat "8.3"). +Notation Zmult_0_r := Z.mul_0_r (compat "8.3"). +Notation Zmult_1_l := Z.mul_1_l (compat "8.3"). +Notation Zmult_1_r := Z.mul_1_r (compat "8.3"). +Notation Zmult_comm := Z.mul_comm (compat "8.3"). +Notation Zmult_assoc := Z.mul_assoc (compat "8.3"). +Notation Zmult_permute := Z.mul_shuffle3 (compat "8.3"). +Notation Zmult_1_inversion_l := Z.mul_eq_1 (compat "8.3"). +Notation Zdouble_mult := Z.double_spec (compat "8.3"). +Notation Zdouble_plus_one_mult := Z.succ_double_spec (compat "8.3"). +Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (compat "8.3"). +Notation Zmult_opp_opp := Z.mul_opp_opp (compat "8.3"). +Notation Zmult_opp_comm := Z.mul_opp_comm (compat "8.3"). +Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (compat "8.3"). +Notation Zmult_plus_distr_r := Z.mul_add_distr_l (compat "8.3"). +Notation Zmult_plus_distr_l := Z.mul_add_distr_r (compat "8.3"). +Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (compat "8.3"). +Notation Zmult_reg_l := Z.mul_reg_l (compat "8.3"). +Notation Zmult_reg_r := Z.mul_reg_r (compat "8.3"). +Notation Zmult_succ_l := Z.mul_succ_l (compat "8.3"). +Notation Zmult_succ_r := Z.mul_succ_r (compat "8.3"). +Notation Zpos_xI := Z.pos_xI (compat "8.3"). +Notation Zpos_xO := Z.pos_xO (compat "8.3"). +Notation Zneg_xI := Z.neg_xI (compat "8.3"). +Notation Zneg_xO := Z.neg_xO (compat "8.3"). Notation Z := Z (only parsing). Notation Z_rect := Z_rect (only parsing). |