Commit 9d7640c0 authored by Robbert Krebbers's avatar Robbert Krebbers

Revert "`RelDecision` instance for `flip`, and make `flip` tc opaque to avoid...

Revert "`RelDecision` instance for `flip`, and make `flip` tc opaque to avoid loops due to eager unification."

This reverts commit b81aa3aa.
parent b81aa3aa
......@@ -505,12 +505,7 @@ Arguments id _ _ / : assert.
Arguments compose _ _ _ _ _ _ / : assert.
Arguments flip _ _ _ _ _ _ / : assert.
Arguments const _ _ _ _ / : assert.
Typeclasses Transparent id compose const.
(** Make sure that [flip] is type class opaque, otherwise one gets loops due to
instance involving [flip], e.g. [RelDecision R → RelDecision (flip R)] could be
used indefinitely. *)
Typeclasses Opaque flip.
Typeclasses Transparent id compose flip const.
Definition fun_map {A A' B B'} (f: A' A) (g: B B') (h : A B) : A' B' :=
g h f.
......
......@@ -135,7 +135,7 @@ Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
dexist (`x) p = x.
Proof. apply dsig_eq; reflexivity. Qed.
(** * Instances of [Decision] *)
(** * Instances of Decision *)
(** Instances of [Decision] for operators of propositional logic. *)
Instance True_dec: Decision True := left I.
Instance False_dec: Decision False := right (False_rect False).
......@@ -192,7 +192,3 @@ Proof. destruct (decide Q); tauto. Qed.
Program Definition inj_eq_dec `{EqDecision A} {B} (f : B A)
`{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
Solve Obligations with firstorder congruence.
(** * Instances of [RelDecision] *)
Instance flip_dec {A} (R : relation A) `{!RelDecision R} :
RelDecision (flip R) := λ x y, decide_rel R y x.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment