Skip to content

Commit

Permalink
Add regression test for issue #614.
Browse files Browse the repository at this point in the history
  • Loading branch information
Brian Huffman committed Dec 13, 2019
1 parent ccd388d commit 4b29967
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 0 deletions.
6 changes: 6 additions & 0 deletions tests/issues/issue614.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
f : {m, n, k} (n == max 2 m k == m + 1) => [m] -> [k][n]
f x = zero


g : {n, k} (fin n, fin k, 0 < n <= k) => [n] -> [k]
g x = sext x
1 change: 1 addition & 0 deletions tests/issues/issue614.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
:l issue614.cry
16 changes: 16 additions & 0 deletions tests/issues/issue614.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main

[error] at issue614.cry:1:18--1:20 and issue614.cry:1:31--1:33
The fixities of
• (==) (precedence 20, non-associative)
• (==) (precedence 20, non-associative)
are not compatible.
You may use explicit parentheses to disambiguate.
[error] at issue614.cry:5:29--5:30 and issue614.cry:5:33--5:35
The fixities of
• (<) (precedence 30, non-associative)
• (<=) (precedence 30, non-associative)
are not compatible.
You may use explicit parentheses to disambiguate.

0 comments on commit 4b29967

Please sign in to comment.