Skip to content
Snippets Groups Projects

Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available.

Merged Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available.
mattam82/stdpp:coq-13969 into master
1 unresolved thread
Merged Matthieu Sozeau requested to merge mattam82/stdpp:coq-13969 into master
1 unresolved thread
Compare
and
1 file
+ 7
− 0
Compare changes
  • Side-by-side
  • Inline
theories/base.v
+ 7
− 0
@@ -251,6 +251,13 @@ Class Equiv A := equiv: relation A.
@@ -251,6 +251,13 @@ Class Equiv A := equiv: relation A.
fixed in Coq >= 8.12.
fixed in Coq >= 8.12.
Global Hint Mode Equiv ! : typeclass_instances. *)
Global Hint Mode Equiv ! : typeclass_instances. *)
 
(** We instruct setoid rewriting to infer [equiv] as a relation on
 
type [A] when needed. This allows setoid_rewrite to solve constraints
 
of shape [Proper (eq ==> ?R) f] using [Proper (eq ==> (equiv (A:=A))) f]
 
when an equivalence relation is available on type [A]. *)
 
Global Instance equiv_rewrite_relation `{Equiv A} :
 
RewriteRelation (@equiv A _) := {}.
 
Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
Infix "≡@{ A }" := (@equiv A _)
Infix "≡@{ A }" := (@equiv A _)
(at level 70, only parsing, no associativity) : stdpp_scope.
(at level 70, only parsing, no associativity) : stdpp_scope.