Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add splitAt function to Cryptol book #1771

Open
marsella opened this issue Nov 19, 2024 · 2 comments
Open

Add splitAt function to Cryptol book #1771

marsella opened this issue Nov 19, 2024 · 2 comments
Labels
book The "Programming in Cryptol" book

Comments

@marsella
Copy link
Contributor

The splitAt function isn't in the book!

> :h splitAt 

    splitAt : {front, back, a}
      (fin front) =>
      [front + back]a -> ([front]a, [back]a)

Splits a sequence into a pair of sequences.
'splitAt z = (x, y)' iff 'x # y = z'.

We should add it, at least to Appendix B (the cryptol prelude description).

@marsella marsella added the book The "Programming in Cryptol" book label Nov 19, 2024
@RyanGlScott
Copy link
Contributor

Interestingly, there is a commented-out section at the end of the book (here) that includes splitAt as well as some other functions. After scavenging splitAt out of this commented-out section, we should see if any of the other functions in that section also need to be mentioned in the book.

@yav
Copy link
Member

yav commented Nov 21, 2024

When we update the book it might make sense to also point out the relation between splitAt and # patterns.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
book The "Programming in Cryptol" book
Projects
None yet
Development

No branches or pull requests

3 participants