diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-04 16:02:24 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-04 16:02:24 +0000 |
| commit | 2b4c3fff22d7e9c55289c2fe770e744b7a5f613c (patch) | |
| tree | 21d1cb9bd91cc2d91a8077ccfe9bdf0ac9d6e69b /theories/Numbers/Natural/BigN | |
| parent | ff03e8dd0de507be82e58ed5e8fd902dfd7caf4b (diff) | |
Fix bug #1899: no more strange notations for Qge and Qgt
In fact, Qge and Ggt disappear, and we only leave notations for > and >=
that map directly to Qlt and Qle.
We also adopt the same approach for BigN, BigZ, BigQ.
By the way, various clean-up concerning Zeq_bool, Zle_bool and similar
functions for Q.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11205 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/BigN')
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 1e0b45cd2..653170e34 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -47,6 +47,8 @@ Infix "?=" := BigN.compare : bigN_scope. Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope. Infix "<" := BigN.lt : bigN_scope. Infix "<=" := BigN.le : bigN_scope. +Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope. +Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope. Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. Open Scope bigN_scope. @@ -62,7 +64,7 @@ Qed. (** [BigN] is a semi-ring *) -Lemma BigNring : +Lemma BigNring : semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq. Proof. constructor. |