search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 123 forks source link

generateEnd #1377

Open weaversa opened 2 years ago

weaversa commented 2 years ago

We have indexing and slicing from the left and right with @, @@, ! and !!, but we only have a left-hand generate -- x @ i = ...

Have you considered adding the natural dual, x ! i = ...? This construction would be useful when (for example) building sequences from numbers, where i is the low order bit of x.

weaversa commented 2 years ago

I thought to name it generateEnd because we already use this naming construct with, for example, update and updateEnd.

weaversa commented 2 years ago

This is kind of odd - the nightly accepts the x ! i syntactic sugar...

Cryptol> let x@i = i 
Cryptol> x : [10][10]
[0x000, 0x001, 0x002, 0x003, 0x004, 0x005, 0x006, 0x007, 0x008,
 0x009]
Cryptol> let y!i = i 
Cryptol> y : [10][10]

[error] at <interactive>:4:1--4:2
    Value not in scope: y
yav commented 2 years ago

Without any special treatment, y ! x just defines an infix operator !

yav commented 2 years ago

Added "low-hanging fruit" as it looks like a good ticket for someone looking to get started with Cryptol hacking.