Commit bf6caa7f authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Ralf Jung

Make nclose an explicit coercion.

We do this by introducing a type class UpClose with notation ↑.

The reason for this change is as follows: since `nclose : namespace
→ coPset` is declared as a coercion, the notation `nclose N ⊆ E` was
pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked
because type checking goes from left to right, and as such would look
for an instance `SubsetEq namespace`, which causes the right hand side
to be ill-typed.
parent d109d7bb
...@@ -726,6 +726,8 @@ End disjoint_list. ...@@ -726,6 +726,8 @@ End disjoint_list.
Class Filter A B := filter: (P : A Prop) `{ x, Decision (P x)}, B B. Class Filter A B := filter: (P : A Prop) `{ x, Decision (P x)}, B B.
Class UpClose A B := up_close : A B.
Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
(** * Monadic operations *) (** * Monadic operations *)
(** We define operational type classes for the monadic operations bind, join (** We define operational type classes for the monadic operations bind, join
......
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