diff --git a/tests/issues/issue128.cry b/tests/issues/issue128.cry new file mode 100644 index 00000000..01e044b8 --- /dev/null +++ b/tests/issues/issue128.cry @@ -0,0 +1,4 @@ +copy : [inf] -> [inf] +copy ([b] # x) = if b then [True] # copy x else [False] # copy x + +property ok = copy ([True] # zero) @ 0 diff --git a/tests/issues/issue128.icry b/tests/issues/issue128.icry new file mode 100644 index 00000000..f08fd9a2 --- /dev/null +++ b/tests/issues/issue128.icry @@ -0,0 +1,3 @@ +:l issue128.cry +:check ok +:prove ok diff --git a/tests/issues/issue128.icry.stdout b/tests/issues/issue128.icry.stdout new file mode 100644 index 00000000..d3dedc42 --- /dev/null +++ b/tests/issues/issue128.icry.stdout @@ -0,0 +1,7 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +Using exhaustive testing. +passed 1 tests. +Q.E.D. +Q.E.D.