diff options
Diffstat (limited to 'theories/PArith/Pnat.v')
| -rw-r--r-- | theories/PArith/Pnat.v | 70 |
1 files changed, 36 insertions, 34 deletions
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index 9c2608f4..26aba87f 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -1,10 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import BinPos PeanoNat. @@ -382,36 +384,36 @@ End SuccNat2Pos. (** For compatibility, old names and old-style lemmas *) -Notation Psucc_S := Pos2Nat.inj_succ (compat "8.3"). -Notation Pplus_plus := Pos2Nat.inj_add (compat "8.3"). -Notation Pmult_mult := Pos2Nat.inj_mul (compat "8.3"). -Notation Pcompare_nat_compare := Pos2Nat.inj_compare (compat "8.3"). -Notation nat_of_P_xH := Pos2Nat.inj_1 (compat "8.3"). -Notation nat_of_P_xO := Pos2Nat.inj_xO (compat "8.3"). -Notation nat_of_P_xI := Pos2Nat.inj_xI (compat "8.3"). -Notation nat_of_P_is_S := Pos2Nat.is_succ (compat "8.3"). -Notation nat_of_P_pos := Pos2Nat.is_pos (compat "8.3"). -Notation nat_of_P_inj_iff := Pos2Nat.inj_iff (compat "8.3"). -Notation nat_of_P_inj := Pos2Nat.inj (compat "8.3"). -Notation Plt_lt := Pos2Nat.inj_lt (compat "8.3"). -Notation Pgt_gt := Pos2Nat.inj_gt (compat "8.3"). -Notation Ple_le := Pos2Nat.inj_le (compat "8.3"). -Notation Pge_ge := Pos2Nat.inj_ge (compat "8.3"). -Notation Pminus_minus := Pos2Nat.inj_sub (compat "8.3"). -Notation iter_nat_of_P := @Pos2Nat.inj_iter (compat "8.3"). - -Notation nat_of_P_of_succ_nat := SuccNat2Pos.id_succ (compat "8.3"). -Notation P_of_succ_nat_of_P := Pos2SuccNat.id_succ (compat "8.3"). - -Notation nat_of_P_succ_morphism := Pos2Nat.inj_succ (compat "8.3"). -Notation nat_of_P_plus_morphism := Pos2Nat.inj_add (compat "8.3"). -Notation nat_of_P_mult_morphism := Pos2Nat.inj_mul (compat "8.3"). -Notation nat_of_P_compare_morphism := Pos2Nat.inj_compare (compat "8.3"). -Notation lt_O_nat_of_P := Pos2Nat.is_pos (compat "8.3"). -Notation ZL4 := Pos2Nat.is_succ (compat "8.3"). -Notation nat_of_P_o_P_of_succ_nat_eq_succ := SuccNat2Pos.id_succ (compat "8.3"). -Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (compat "8.3"). -Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (compat "8.3"). +Notation Psucc_S := Pos2Nat.inj_succ (only parsing). +Notation Pplus_plus := Pos2Nat.inj_add (only parsing). +Notation Pmult_mult := Pos2Nat.inj_mul (only parsing). +Notation Pcompare_nat_compare := Pos2Nat.inj_compare (only parsing). +Notation nat_of_P_xH := Pos2Nat.inj_1 (only parsing). +Notation nat_of_P_xO := Pos2Nat.inj_xO (only parsing). +Notation nat_of_P_xI := Pos2Nat.inj_xI (only parsing). +Notation nat_of_P_is_S := Pos2Nat.is_succ (only parsing). +Notation nat_of_P_pos := Pos2Nat.is_pos (only parsing). +Notation nat_of_P_inj_iff := Pos2Nat.inj_iff (only parsing). +Notation nat_of_P_inj := Pos2Nat.inj (only parsing). +Notation Plt_lt := Pos2Nat.inj_lt (only parsing). +Notation Pgt_gt := Pos2Nat.inj_gt (only parsing). +Notation Ple_le := Pos2Nat.inj_le (only parsing). +Notation Pge_ge := Pos2Nat.inj_ge (only parsing). +Notation Pminus_minus := Pos2Nat.inj_sub (only parsing). +Notation iter_nat_of_P := @Pos2Nat.inj_iter (only parsing). + +Notation nat_of_P_of_succ_nat := SuccNat2Pos.id_succ (only parsing). +Notation P_of_succ_nat_of_P := Pos2SuccNat.id_succ (only parsing). + +Notation nat_of_P_succ_morphism := Pos2Nat.inj_succ (only parsing). +Notation nat_of_P_plus_morphism := Pos2Nat.inj_add (only parsing). +Notation nat_of_P_mult_morphism := Pos2Nat.inj_mul (only parsing). +Notation nat_of_P_compare_morphism := Pos2Nat.inj_compare (only parsing). +Notation lt_O_nat_of_P := Pos2Nat.is_pos (only parsing). +Notation ZL4 := Pos2Nat.is_succ (only parsing). +Notation nat_of_P_o_P_of_succ_nat_eq_succ := SuccNat2Pos.id_succ (only parsing). +Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (only parsing). +Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (only parsing). Lemma nat_of_P_minus_morphism p q : Pos.compare_cont Eq p q = Gt -> |