GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-01 04:14:24 +03:00
Code Issues Projects Releases Wiki Activity

Add regression test for #731.

Browse Source
This commit is contained in:
Brian Huffman 2020-05-18 17:17:58 -07:00
parent e1fb6e940d
commit 37f1fd8b4b
3 changed files with 23 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
tests/issues/issue731.cry Normal file
View File

@ -0,0 +1,7 @@
type constraint T n = (fin n, n >= 1)
type constraint Both p q = (p, q)
type constraint Fin2 i j = Both (fin i) (fin j)
type constraint i <=> j = (i <= j, i >= j)

2
tests/issues/issue731.icry Normal file
View File

@ -0,0 +1,2 @@
:l issue731.cry
:browse Main

14
tests/issues/issue731.icry.stdout Normal file
View File

@ -0,0 +1,14 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
Constraint Synonyms
===================
Public
------
type constraint (<=>) i j = (i <= j, i >= j)
type constraint Both p q = (p, q)
type constraint Fin2 i j = Both (fin i) (fin j)
type constraint T n = (fin n, n >= 1)