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

Update expected test output related to #1275 fix.

Browse Source
This commit is contained in:
Brian Huffman 2021-09-02 17:34:12 -07:00
parent 58723d074b
commit f25536aab3
4 changed files with 14 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
tests/issues/issue226.icry.stdout
View File

@ -133,8 +133,8 @@ Symbols
fromThenTo :
{first, next, last, a, len}
(fin first, fin next, fin last, Literal first a, Literal next a,
Literal last a, first != next, lengthFromThenTo first next last ==
len) =>
Literal last a, first != next,
lengthFromThenTo first next last == len) =>
[len]a
fromTo :
{first, last, a}

12
tests/issues/issue268.icry.stdout
View File

@ -1,9 +1,9 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
[(0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00,
0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
(0x00, 0x00)]
[(0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00,
0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
(0x00, 0x00)]
[(0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
(0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
(0x00, 0x00), (0x00, 0x00)]
[(0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
(0x00, 0x00), (0x00, 0x00), (0x00, 0x00), (0x00, 0x00),
(0x00, 0x00), (0x00, 0x00)]

7
tests/issues/issue407.icry.stdout
View File

@ -1,7 +1,8 @@
Loading module Cryptol
[[False, False, False, False, False, ...], [False, False, False,
False, True, ...], [False, False, True, True, False, ...], [False,
True, False, True, False, ...]]
[[False, False, False, False, False, ...],
[False, False, False, False, True, ...],
[False, False, True, True, False, ...],
[False, True, False, True, False, ...]]
Counterexample
(\(x : [4]) -> (transpose [x ...]) @ 0 @ 0 == False) 0x8 = False
Q.E.D.

4
tests/issues/padding.icry.stdout
View File

@ -2,5 +2,5 @@ Loading module Cryptol
Showing a specific instance of polymorphic result:
* Using 'Integer' for type argument 'a' of 'Cryptol::fromTo'
* Using 'inf' for type argument 'parts' of 'Cryptol::groupBy'
[[1, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15], [16, 17,
18, 19, 20], [21, 22, 23, 24, 0], ...]
[[1, 2, 3, 4, 5], [6, 7, 8, 9, 10], [11, 12, 13, 14, 15],
[16, 17, 18, 19, 20], [21, 22, 23, 24, 0], ...]