mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 01:13:34 +03:00
Update test output.
This commit is contained in:
parent
b03f1ae0c2
commit
35423d0243
@ -29,7 +29,7 @@ Symbols
|
||||
(/\) : Bit -> Bit -> Bit
|
||||
(<) : {a} (Cmp a) => a -> a -> Bit
|
||||
(<$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||
(<<) : {a, b, c} (fin b, Logic c) => [a]c -> [b] -> [a]c
|
||||
(<<) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
|
||||
(<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
|
||||
(<=) : {a} (Cmp a) => a -> a -> Bit
|
||||
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||
@ -40,7 +40,7 @@ Symbols
|
||||
(>$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||
(>=) : {a} (Cmp a) => a -> a -> Bit
|
||||
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||
(>>) : {a, b, c} (fin b, Logic c) => [a]c -> [b] -> [a]c
|
||||
(>>) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
|
||||
(>>$) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n]
|
||||
(>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
|
||||
(@) : {a, b, c} (fin c) => [a]b -> [c] -> b
|
||||
@ -106,7 +106,7 @@ Symbols
|
||||
fin d) => [a]b -> [d][c] -> [d]b -> [a]b
|
||||
width : {bits, len, elem} (fin len, fin bits,
|
||||
bits >= width len) => [len]elem -> [bits]
|
||||
zero : {a} (Logic a) => a
|
||||
zero : {a} (Zero a) => a
|
||||
zext : {n, m} (fin m, m >= n) => [n] -> [m]
|
||||
(||) : {a} (Logic a) => a -> a -> a
|
||||
|
||||
|
@ -14,8 +14,8 @@ test05::foo : [10]
|
||||
test05::foo = Cryptol::demote 10 10 <> <> <>
|
||||
|
||||
/* Not recursive */
|
||||
test05::test : {a, b, c} (Logic b, fin c, c >= 4) => [a]b -> [c]
|
||||
test05::test = \{a, b, c} (Logic b, fin c, c >= 4) (a : [a]b) ->
|
||||
test05::test : {a, b, c} (Zero b, fin c, c >= 4) => [a]b -> [c]
|
||||
test05::test = \{a, b, c} (Zero b, fin c, c >= 4) (a : [a]b) ->
|
||||
Cryptol::demote 10 c <> <> <>
|
||||
where
|
||||
/* Not recursive */
|
||||
@ -60,8 +60,8 @@ test05::foo : [10]
|
||||
test05::foo = Cryptol::demote 10 10 <> <> <>
|
||||
|
||||
/* Not recursive */
|
||||
test05::test : {a, b, c} (Logic b, fin c, c >= 4) => [a]b -> [c]
|
||||
test05::test = \{a, b, c} (Logic b, fin c, c >= 4) (a : [a]b) ->
|
||||
test05::test : {a, b, c} (Zero b, fin c, c >= 4) => [a]b -> [c]
|
||||
test05::test = \{a, b, c} (Zero b, fin c, c >= 4) (a : [a]b) ->
|
||||
Cryptol::demote 10 c <> <> <>
|
||||
where
|
||||
/* Not recursive */
|
||||
|
@ -1,6 +1,6 @@
|
||||
module test06 where
|
||||
|
||||
test : {a} (Logic a) => a -> a
|
||||
test : {a} (Zero a) => a -> a
|
||||
test a = bar
|
||||
where
|
||||
foo : a
|
||||
|
@ -4,8 +4,8 @@ Loading module test06
|
||||
module test06
|
||||
import Cryptol
|
||||
/* Not recursive */
|
||||
test06::test : {a} (Logic a) => a -> a
|
||||
test06::test = \{a} (Logic a) (a : a) ->
|
||||
test06::test : {a} (Zero a) => a -> a
|
||||
test06::test = \{a} (Zero a) (a : a) ->
|
||||
test06::bar
|
||||
where
|
||||
/* Not recursive */
|
||||
@ -23,8 +23,8 @@ Loading module test06
|
||||
module test06
|
||||
import Cryptol
|
||||
/* Not recursive */
|
||||
test06::test : {a} (Logic a) => a -> a
|
||||
test06::test = \{a} (Logic a) (a : a) ->
|
||||
test06::test : {a} (Zero a) => a -> a
|
||||
test06::test = \{a} (Zero a) (a : a) ->
|
||||
test06::bar
|
||||
where
|
||||
/* Not recursive */
|
||||
|
Loading…
Reference in New Issue
Block a user