Skip to content

GitLab

Commit c0793382 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Hint Mode for LimitPreserving.

parent 1f1c66bd
Hide whitespace changes
Inline Side-by-side
theories/algebra/ofe.v
View file @ c0793382
...@@ -1073,7 +1073,8 @@ Qed. ...@@ -1073,7 +1073,8 @@ Qed.
(** Sigma *) (** Sigma *)
Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop := Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=
limit_preserving : ∀ c : chain A, (∀ n, P (c n)) → P (compl c). limit_preserving (c : chain A) : (∀ n, P (c n)) → P (compl c).
Hint Mode LimitPreserving + + ! : typeclass_instances.
Section limit_preserving. Section limit_preserving.
Context {A : ofeT} `{!Cofe A}. Context {A : ofeT} `{!Cofe A}.
......
Supports Markdown
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