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
  • Issues
  • #322
Closed
Open
Issue created May 28, 2020 by Dmitry Khalanskiy@dkhalanskiyjbContributor

Operator precedence in heap lang is wrong

The Iris version is dev.2020-05-18.2.fdda97e8.

Given the definition

Definition v: expr := #true || #false = #false.

I expect it to read the same as in most other languages: "Either true is true or false is equal to false". However, Print v shows:

v = ((if: #true then #true else #false) = #false)%E
     : expr

In other words, || has higher precedence than comparisons. I'm not familiar with how exactly notations in Coq are specified, but, looking at notation.v, it seems that precedence for common operators is not specified explicitly but is instead inherited from other notations that are known to Coq, and in vanilla Coq = has low precedence, given its role.

Edited May 28, 2020 by Dmitry Khalanskiy
Assignee
Assign to
Time tracking