Add regression test for issue #614.

This commit is contained in:
Brian Huffman 2019-12-13 11:13:03 -08:00
parent ccd388da2a
commit 4b29967315
3 changed files with 23 additions and 0 deletions

View File

@ -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

View File

@ -0,0 +1 @@
:l issue614.cry

View File

@ -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.