Forked from
Iris / Iris
Source project has a limited visibility.
-
Ralf Jung authored
Use notation N @⊆ E to avoid ambiguity. 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. See merge request !24
Ralf Jung authoredUse notation N @⊆ E to avoid ambiguity. 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. See merge request !24
To find the state of this project's repository at the time of any of these versions, check out the tags.