mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-01 08:32:23 +03:00
1.7 KiB
1.7 KiB
Summary of Changes
| Cryptol version 2 | Cryptol version 1 | Summary |
|---|---|---|
[ False, True, True ] (==3) |
[ False True True ] (== 6) |
Big-endian word representation |
[ 1, 1, 2, 3, 5 ] |
[ 1 1 2 3 5 ] |
Commas separate sequence entries |
x = 1 |
x = 1; |
Uses layout instead of ;'s and {'s |
| `[ x | x <- [1 .. 10] ]` | `[ |
f : {a,b} a -> b |
f : {a b} a -> b |
Commas separate type variables |
take`{1} xs |
take(1, xs) |
First-class type parameters |
x ^^ 2 |
x ** 2 |
^^ for exponentiation |
| `< | x^^2 + 1 | >` |
[0 ..]:[_][8] |
take(255, [0 ..]:[inf][8]) |
Both produce [0 .. 255] |
[0 ...]:[inf][8] |
[0 ..]:[inf][8] |
Both produce [0 .. 255](repeated) |
[9, 8 .. 0] |
[9 -- 0] |
Step defines decreasing sequences |
| `&&, | , ^` | |
property foo xs=... |
theorem foo: {xs}. xs==... |
Properties replace theorems (see below) |