Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
iris-coq
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Jeehoon Kang
iris-coq
Commits
24fa20e5
Commit
24fa20e5
authored
Feb 11, 2016
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
prelude: add notation for > and >= for all kinds of numbers
parent
f01228f2
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
21 additions
and
0 deletions
+21
-0
prelude/numbers.v
prelude/numbers.v
+21
-0
No files found.
prelude/numbers.v
View file @
24fa20e5
...
...
@@ -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