search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

Add support for numeric constraint guards in properties #1765

Open marsella opened 2 hours ago

marsella commented 2 hours ago

Right now, properties do not compile with a numeric constraint guard. The example:

f : {n} [n] -> Bit
property f _
  | n == 1 => True
  | n != 1 => False

produces the following error:

Parse error at [...] unexpected: |

The same function compiles if you remove the property annotation. It would be useful to use numeric constraint guards in properties.

marsella commented 2 hours ago

Oh oops. This is a duplicate of #1595.