Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Simon Spies
stdpp
Commits
f4192019
Commit
f4192019
authored
Feb 11, 2016
by
Ralf Jung
Browse files
prelude: add notation for > and >= for all kinds of numbers
parent
f024eb62
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
21 additions
and
0 deletions
+21
-0
theories/numbers.v
theories/numbers.v
+21
-0
No files found.
theories/numbers.v
View file @
f4192019
...
...
@@ -28,6 +28,10 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_
Notation
"(≤)"
:
=
le
(
only
parsing
)
:
nat_scope
.
Notation
"(<)"
:
=
lt
(
only
parsing
)
:
nat_scope
.
Infix
"≥"
:
=
ge
:
nat_scope
.
Notation
"(≥)"
:
=
ge
(
only
parsing
)
:
nat_scope
.
Notation
"(>)"
:
=
gt
(
only
parsing
)
:
nat_scope
.
Infix
"`div`"
:
=
Nat
.
div
(
at
level
35
)
:
nat_scope
.
Infix
"`mod`"
:
=
Nat
.
modulo
(
at
level
35
)
:
nat_scope
.
...
...
@@ -104,6 +108,10 @@ Notation "(<)" := Pos.lt (only parsing) : positive_scope.
Notation
"(~0)"
:
=
xO
(
only
parsing
)
:
positive_scope
.
Notation
"(~1)"
:
=
xI
(
only
parsing
)
:
positive_scope
.
Infix
"≥"
:
=
Pos
.
ge
:
positive_scope
.
Notation
"(≥)"
:
=
Pos
.
ge
(
only
parsing
)
:
positive_scope
.
Notation
"(>)"
:
=
Pos
.
gt
(
only
parsing
)
:
positive_scope
.
Arguments
Pos
.
of_nat
_
:
simpl
never
.
Instance
positive_eq_dec
:
∀
x
y
:
positive
,
Decision
(
x
=
y
)
:
=
Pos
.
eq_dec
.
Instance
positive_inhabited
:
Inhabited
positive
:
=
populate
1
.
...
...
@@ -179,6 +187,11 @@ Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope.
Notation
"x ≤ y ≤ z ≤ z'"
:
=
(
x
≤
y
∧
y
≤
z
∧
z
≤
z'
)%
N
:
N_scope
.
Notation
"(≤)"
:
=
N
.
le
(
only
parsing
)
:
N_scope
.
Notation
"(<)"
:
=
N
.
lt
(
only
parsing
)
:
N_scope
.
Infix
"≥"
:
=
N
.
ge
:
N_scope
.
Notation
"(≥)"
:
=
N
.
ge
(
only
parsing
)
:
N_scope
.
Notation
"(>)"
:
=
N
.
gt
(
only
parsing
)
:
N_scope
.
Infix
"`div`"
:
=
N
.
div
(
at
level
35
)
:
N_scope
.
Infix
"`mod`"
:
=
N
.
modulo
(
at
level
35
)
:
N_scope
.
...
...
@@ -213,6 +226,10 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Z_scope.
Notation
"(≤)"
:
=
Z
.
le
(
only
parsing
)
:
Z_scope
.
Notation
"(<)"
:
=
Z
.
lt
(
only
parsing
)
:
Z_scope
.
Infix
"≥"
:
=
Z
.
ge
:
Z_scope
.
Notation
"(≥)"
:
=
Z
.
ge
(
only
parsing
)
:
Z_scope
.
Notation
"(>)"
:
=
Z
.
gt
(
only
parsing
)
:
Z_scope
.
Infix
"`div`"
:
=
Z
.
div
(
at
level
35
)
:
Z_scope
.
Infix
"`mod`"
:
=
Z
.
modulo
(
at
level
35
)
:
Z_scope
.
Infix
"`quot`"
:
=
Z
.
quot
(
at
level
35
)
:
Z_scope
.
...
...
@@ -328,6 +345,10 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Qc_scope
Notation
"(≤)"
:
=
Qcle
(
only
parsing
)
:
Qc_scope
.
Notation
"(<)"
:
=
Qclt
(
only
parsing
)
:
Qc_scope
.
Infix
"≥"
:
=
Qcge
:
Qc_scope
.
Notation
"(≥)"
:
=
Qcge
(
only
parsing
)
:
Qc_scope
.
Notation
"(>)"
:
=
Qcgt
(
only
parsing
)
:
Qc_scope
.
Hint
Extern
1
(
_
≤
_
)
=>
reflexivity
||
discriminate
.
Arguments
Qred
_
:
simpl
never
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment