Skip to content

Use notation N @⊆ E to avoid ambiguity.

Robbert Krebbers requested to merge nclose_subseteq into master

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.

Merge request reports