GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 22:17:18 +03:00
Code Issues Projects Releases Wiki Activity

Add examples of x @ i = e syntax to Syntax.md.

Browse Source
This commit is contained in:
Brian Huffman 2019-06-19 11:25:30 -07:00
parent 088126076e
commit 8d2f1ed2ba
1 changed files with 11 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
docs/Syntax.md
View File

@ -379,16 +379,21 @@ _word_. We may abbreviate the type `[n] Bit` as `[n]`. An infinite
sequence with elements of type `a` has type `[inf] a`, and `[inf]` is
an infinite stream of bits.
[e1,e2,e3] // A sequence with three elements
[e1,e2,e3] // A sequence with three elements
[t1 .. t3 ] // Sequence enumerations
[t1, t2 .. t3 ] // Step by t2 - t1
[e1 ... ] // Infinite sequence starting at e1
[e1, e2 ... ] // Infinite sequence stepping by e2-e1
[t1 .. t3 ] // Sequence enumerations
[t1, t2 .. t3 ] // Step by t2 - t1
[e1 ... ] // Infinite sequence starting at e1
[e1, e2 ... ] // Infinite sequence stepping by e2-e1
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
| p21 <- e21, p22 <- e22 ]
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
Note: the bounds in finite sequences (those with `..`) are type
expressions, while the bounds in infinite sequences are value
expressions.