You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
$ docker run --rm -it ghcr.io/galoisinc/cryptol:nightly
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃ ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹ ╹ ┗━┛┗━╸
version 2.13.0.99
https://cryptol.net :? for help
Loading module Cryptol
Cryptol> (-3:Integer) <$ 5
[error] at <interactive>:1:1--1:18:
• Type `Integer` does not support signed comparisons.
arising from
use of expression (<$)
at <interactive>:1:1--1:18
Should it?
The text was updated successfully, but these errors were encountered:
> :h <$
(<$) : {a} (SignedCmp a) => a -> a -> Bit
Precedence 30, does not associate.
2's complement signed less-than.
Integers are not "2's complement".
Cryptol> :h <
type constraint i < j = j >= 1 + i
Assert that the first numeric type is less than the second.
---------
(<) : {a} (Cmp a) => a -> a -> Bit
Precedence 30, does not associate.
Less-than. Only works on comparable arguments.
Bitvectors are compared using unsigned arithmetic.
Integers are not bitvectors, so comparison is not "unsigned" and the type constraint applies. Makes sense.
Should it?
The text was updated successfully, but these errors were encountered: