Commit 71fb10bd authored by Robbert Krebbers's avatar Robbert Krebbers

Set `Hint Mode` for `Cofe`.

parent 4f0c1046
......@@ -125,6 +125,7 @@ Class Cofe (A : ofeT) := {
conv_compl n c : compl c {n} c n;
Arguments compl : simpl never.
Hint Mode Cofe ! : typeclass_instances.
Lemma compl_chain_map `{Cofe A, Cofe B} (f : A B) c `(NonExpansive f) :
compl (chain_map f c) f (compl c).
......@@ -264,7 +265,7 @@ Section limit_preserving.
( x, P x Q x) LimitPreserving P LimitPreserving Q.
Proof. intros HP Hlimit c ?. apply HP, Hlimit=> n; by apply HP. Qed.
Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _, P).
Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _ : A, P).
Proof. intros c HP. apply (HP 0). Qed.
Lemma limit_preserving_discrete (P : A Prop) :
......@@ -402,7 +402,7 @@ Lemma entails_lim (cP cQ : chain (uPredO M)) :
( n, cP n cQ n) compl cP compl cQ.
intros Hlim; split=> n m ? HP.
eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl.
eapply uPred_holds_ne, Hlim, HP; rewrite ?conv_compl; eauto.
(** Non-expansiveness and setoid morphisms *)
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment