From 37f1fd8b4b51b375e9ef3cb7f4e4d3879c7e2ebc Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 18 May 2020 17:17:58 -0700 Subject: [PATCH] Add regression test for #731. --- tests/issues/issue731.cry | 7 +++++++ tests/issues/issue731.icry | 2 ++ tests/issues/issue731.icry.stdout | 14 ++++++++++++++ 3 files changed, 23 insertions(+) create mode 100644 tests/issues/issue731.cry create mode 100644 tests/issues/issue731.icry create mode 100644 tests/issues/issue731.icry.stdout diff --git a/tests/issues/issue731.cry b/tests/issues/issue731.cry new file mode 100644 index 00000000..726a6605 --- /dev/null +++ b/tests/issues/issue731.cry @@ -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) diff --git a/tests/issues/issue731.icry b/tests/issues/issue731.icry new file mode 100644 index 00000000..241ac198 --- /dev/null +++ b/tests/issues/issue731.icry @@ -0,0 +1,2 @@ +:l issue731.cry +:browse Main diff --git a/tests/issues/issue731.icry.stdout b/tests/issues/issue731.icry.stdout new file mode 100644 index 00000000..970bf839 --- /dev/null +++ b/tests/issues/issue731.icry.stdout @@ -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) +