Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 23
    • Merge requests 23
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !24

Use notation N @⊆ E to avoid ambiguity.

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge nclose_subseteq into master Nov 18, 2016
  • Overview 21
  • Commits 3
  • Pipelines 0
  • Changes 16

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.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: nclose_subseteq