Commit 8e83b473 authored by Ralf Jung's avatar Ralf Jung

tweak sigma COFE

parent e7266df5
Pipeline #3595 passed with stage
in 10 minutes and 30 seconds
...@@ -956,7 +956,7 @@ Proof. ...@@ -956,7 +956,7 @@ Proof.
Qed. Qed.
(** Sigma *) (** Sigma *)
Class LimitPreserving {A : ofeT} `{!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).
Section sigma. Section sigma.
...@@ -987,7 +987,7 @@ Section sigma. ...@@ -987,7 +987,7 @@ Section sigma.
Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin. Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin.
(* FIXME: WTF, it seems that within these braces {...} the ofe argument of LimitPreserving (* FIXME: WTF, it seems that within these braces {...} the ofe argument of LimitPreserving
suddenyl becomes explicit...? *) suddenly becomes explicit...? *)
Program Definition sig_compl `{LimitPreserving _ P} : Compl sigC := Program Definition sig_compl `{LimitPreserving _ P} : Compl sigC :=
λ c, exist P (compl (chain_map proj1_sig c)) _. λ c, exist P (compl (chain_map proj1_sig c)) _.
Next Obligation. Next Obligation.
...@@ -1009,7 +1009,7 @@ Section sigma. ...@@ -1009,7 +1009,7 @@ Section sigma.
Qed. Qed.
End sigma. End sigma.
Arguments sigC {A} P. Arguments sigC {_} _.
(** Notation for writing functors *) (** Notation for writing functors *)
Notation "∙" := idCF : cFunctor_scope. Notation "∙" := idCF : cFunctor_scope.
......
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