diff options
Diffstat (limited to 'theories/NArith/BinNat.v')
| -rw-r--r-- | theories/NArith/BinNat.v | 80 |
1 files changed, 41 insertions, 39 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 5d3ec5ab..92c124ec 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) +Numeral Notation N N.of_uint N.to_uint : N_scope. + Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. Infix "*" := N.mul : N_scope. @@ -964,33 +966,33 @@ Notation N_ind := N_ind (only parsing). Notation N0 := N0 (only parsing). Notation Npos := N.pos (only parsing). -Notation Ndiscr := N.discr (compat "8.6"). +Notation Ndiscr := N.discr (compat "8.7"). Notation Ndouble_plus_one := N.succ_double (only parsing). -Notation Ndouble := N.double (compat "8.6"). -Notation Nsucc := N.succ (compat "8.6"). -Notation Npred := N.pred (compat "8.6"). -Notation Nsucc_pos := N.succ_pos (compat "8.6"). -Notation Ppred_N := Pos.pred_N (compat "8.6"). +Notation Ndouble := N.double (compat "8.7"). +Notation Nsucc := N.succ (compat "8.7"). +Notation Npred := N.pred (compat "8.7"). +Notation Nsucc_pos := N.succ_pos (compat "8.7"). +Notation Ppred_N := Pos.pred_N (compat "8.7"). Notation Nplus := N.add (only parsing). Notation Nminus := N.sub (only parsing). Notation Nmult := N.mul (only parsing). -Notation Neqb := N.eqb (compat "8.6"). -Notation Ncompare := N.compare (compat "8.6"). -Notation Nlt := N.lt (compat "8.6"). -Notation Ngt := N.gt (compat "8.6"). -Notation Nle := N.le (compat "8.6"). -Notation Nge := N.ge (compat "8.6"). -Notation Nmin := N.min (compat "8.6"). -Notation Nmax := N.max (compat "8.6"). -Notation Ndiv2 := N.div2 (compat "8.6"). -Notation Neven := N.even (compat "8.6"). -Notation Nodd := N.odd (compat "8.6"). -Notation Npow := N.pow (compat "8.6"). -Notation Nlog2 := N.log2 (compat "8.6"). +Notation Neqb := N.eqb (compat "8.7"). +Notation Ncompare := N.compare (compat "8.7"). +Notation Nlt := N.lt (compat "8.7"). +Notation Ngt := N.gt (compat "8.7"). +Notation Nle := N.le (compat "8.7"). +Notation Nge := N.ge (compat "8.7"). +Notation Nmin := N.min (compat "8.7"). +Notation Nmax := N.max (compat "8.7"). +Notation Ndiv2 := N.div2 (compat "8.7"). +Notation Neven := N.even (compat "8.7"). +Notation Nodd := N.odd (compat "8.7"). +Notation Npow := N.pow (compat "8.7"). +Notation Nlog2 := N.log2 (compat "8.7"). Notation nat_of_N := N.to_nat (only parsing). Notation N_of_nat := N.of_nat (only parsing). -Notation N_eq_dec := N.eq_dec (compat "8.6"). +Notation N_eq_dec := N.eq_dec (compat "8.7"). Notation Nrect := N.peano_rect (only parsing). Notation Nrect_base := N.peano_rect_base (only parsing). Notation Nrect_step := N.peano_rect_succ (only parsing). @@ -999,11 +1001,11 @@ Notation Nrec := N.peano_rec (only parsing). Notation Nrec_base := N.peano_rec_base (only parsing). Notation Nrec_succ := N.peano_rec_succ (only parsing). -Notation Npred_succ := N.pred_succ (compat "8.6"). +Notation Npred_succ := N.pred_succ (compat "8.7"). Notation Npred_minus := N.pred_sub (only parsing). -Notation Nsucc_pred := N.succ_pred (compat "8.6"). +Notation Nsucc_pred := N.succ_pred (compat "8.7"). Notation Ppred_N_spec := N.pos_pred_spec (only parsing). -Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.6"). +Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.7"). Notation Ppred_Nsucc := N.pos_pred_succ (only parsing). Notation Nplus_0_l := N.add_0_l (only parsing). Notation Nplus_0_r := N.add_0_r (only parsing). @@ -1011,7 +1013,7 @@ Notation Nplus_comm := N.add_comm (only parsing). Notation Nplus_assoc := N.add_assoc (only parsing). Notation Nplus_succ := N.add_succ_l (only parsing). Notation Nsucc_0 := N.succ_0_discr (only parsing). -Notation Nsucc_inj := N.succ_inj (compat "8.6"). +Notation Nsucc_inj := N.succ_inj (compat "8.7"). Notation Nminus_N0_Nle := N.sub_0_le (only parsing). Notation Nminus_0_r := N.sub_0_r (only parsing). Notation Nminus_succ_r:= N.sub_succ_r (only parsing). @@ -1021,29 +1023,29 @@ Notation Nmult_1_r := N.mul_1_r (only parsing). Notation Nmult_comm := N.mul_comm (only parsing). Notation Nmult_assoc := N.mul_assoc (only parsing). Notation Nmult_plus_distr_r := N.mul_add_distr_r (only parsing). -Notation Neqb_eq := N.eqb_eq (compat "8.6"). +Notation Neqb_eq := N.eqb_eq (compat "8.7"). Notation Nle_0 := N.le_0_l (only parsing). -Notation Ncompare_refl := N.compare_refl (compat "8.6"). +Notation Ncompare_refl := N.compare_refl (compat "8.7"). Notation Ncompare_Eq_eq := N.compare_eq (only parsing). Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing). -Notation Nlt_irrefl := N.lt_irrefl (compat "8.6"). -Notation Nlt_trans := N.lt_trans (compat "8.6"). +Notation Nlt_irrefl := N.lt_irrefl (compat "8.7"). +Notation Nlt_trans := N.lt_trans (compat "8.7"). Notation Nle_lteq := N.lt_eq_cases (only parsing). -Notation Nlt_succ_r := N.lt_succ_r (compat "8.6"). -Notation Nle_trans := N.le_trans (compat "8.6"). -Notation Nle_succ_l := N.le_succ_l (compat "8.6"). -Notation Ncompare_spec := N.compare_spec (compat "8.6"). +Notation Nlt_succ_r := N.lt_succ_r (compat "8.7"). +Notation Nle_trans := N.le_trans (compat "8.7"). +Notation Nle_succ_l := N.le_succ_l (compat "8.7"). +Notation Ncompare_spec := N.compare_spec (compat "8.7"). Notation Ncompare_0 := N.compare_0_r (only parsing). Notation Ndouble_div2 := N.div2_double (only parsing). Notation Ndouble_plus_one_div2 := N.div2_succ_double (only parsing). -Notation Ndouble_inj := N.double_inj (compat "8.6"). +Notation Ndouble_inj := N.double_inj (compat "8.7"). Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing). -Notation Npow_0_r := N.pow_0_r (compat "8.6"). -Notation Npow_succ_r := N.pow_succ_r (compat "8.6"). -Notation Nlog2_spec := N.log2_spec (compat "8.6"). -Notation Nlog2_nonpos := N.log2_nonpos (compat "8.6"). -Notation Neven_spec := N.even_spec (compat "8.6"). -Notation Nodd_spec := N.odd_spec (compat "8.6"). +Notation Npow_0_r := N.pow_0_r (compat "8.7"). +Notation Npow_succ_r := N.pow_succ_r (compat "8.7"). +Notation Nlog2_spec := N.log2_spec (compat "8.7"). +Notation Nlog2_nonpos := N.log2_nonpos (compat "8.7"). +Notation Neven_spec := N.even_spec (compat "8.7"). +Notation Nodd_spec := N.odd_spec (compat "8.7"). Notation Nlt_not_eq := N.lt_neq (only parsing). Notation Ngt_Nlt := N.gt_lt (only parsing). |