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
C
coq-stdpp
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
David Swasey
coq-stdpp
Commits
8b4630b4
Commit
8b4630b4
authored
Dec 05, 2017
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
typeclass comments
parent
9a5be071
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
5 additions
and
2 deletions
+5
-2
theories/base.v
theories/base.v
+5
-2
No files found.
theories/base.v
View file @
8b4630b4
...
...
@@ -119,8 +119,9 @@ Instance: @PreOrder A (=).
Proof
.
split
;
repeat
intro
;
congruence
.
Qed
.
(** ** Setoid equality *)
(** We define an operational type class for setoid equality. This is based on
(Spitters/van der Weegen, 2011). *)
(** We define an operational type class for setoid equality, i.e., the
"canonical" equivalence for a type. The typeclass is tied to the \equiv
symbol. This is based on (Spitters/van der Weegen, 2011). *)
Class
Equiv
A
:
=
equiv
:
relation
A
.
(* No Hint Mode set because of Coq bug #5735
Hint Mode Equiv ! : typeclass_instances. *)
...
...
@@ -1118,6 +1119,8 @@ Notation "½" := half : stdpp_scope.
Notation
"½*"
:
=
(
fmap
(
M
:
=
list
)
half
)
:
stdpp_scope
.
(** * Notations for lattices. *)
(** SqSubsetEq registers the "canonical" partial order for a type, and is used
for the \sqsubseteq symbol. *)
Class
SqSubsetEq
A
:
=
sqsubseteq
:
relation
A
.
Hint
Mode
SqSubsetEq
!
:
typeclass_instances
.
Instance
:
Params
(@
sqsubseteq
)
2
.
...
...
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