GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-24 00:12:22 +03:00
Code Issues Projects Releases Wiki Activity

Add regression test for issue #128.

Browse Source
This commit is contained in:
Brian Huffman 2014-10-23 14:20:04 -07:00
parent fde77d79f3
commit 234aa3230c
3 changed files with 14 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
tests/issues/issue128.cry Normal file
View File

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

3
tests/issues/issue128.icry Normal file
View File

@ -0,0 +1,3 @@
:l issue128.cry
:check ok
:prove ok

7
tests/issues/issue128.icry.stdout Normal file
View File

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