GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-05 15:07:12 +03:00
Code Issues Projects Releases Wiki Activity

Add regression tests for issue #135.

Browse Source
This commit is contained in:
Brian Huffman 2014-11-04 12:03:07 -08:00
parent 80ec38fcf5
commit 0a7b39f944
2 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -0,0 +1,2 @@
:sat \(x : Bit) (y : Bit) -> x < y
:prove \(x : Bit) (y : Bit) -> x <= y || y <= x

3
tests/issues/issue135.icry.stdout Normal file
View File

@ -0,0 +1,3 @@
Loading module Cryptol
(\(x : Bit) (y : Bit) -> x < y) False True = True
Q.E.D.