Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Matthieu Sozeau
stdpp
Commits
b48d40e9
Commit
b48d40e9
authored
Jun 04, 2021
by
Robbert Krebbers
Browse files
Use `!` instead of `+`.
parent
5e3d8b90
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/base.v
View file @
b48d40e9
...
...
@@ -465,13 +465,13 @@ Class PartialOrder {A} (R : relation A) : Prop := {
partial_order_pre
:
>
PreOrder
R
;
partial_order_anti_symm
:
>
AntiSymm
(=)
R
}.
Global
Hint
Mode
PartialOrder
!
+
:
typeclass_instances
.
Global
Hint
Mode
PartialOrder
!
!
:
typeclass_instances
.
Class
TotalOrder
{
A
}
(
R
:
relation
A
)
:
Prop
:
=
{
total_order_partial
:
>
PartialOrder
R
;
total_order_trichotomy
:
>
Trichotomy
(
strict
R
)
}.
Global
Hint
Mode
TotalOrder
!
+
:
typeclass_instances
.
Global
Hint
Mode
TotalOrder
!
!
:
typeclass_instances
.
(** * Logic *)
Global
Instance
prop_inhabited
:
Inhabited
Prop
:
=
populate
True
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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