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

Ex: 1.51 in Cryptol Textbook #887

Closed
manleykm opened this issue Sep 11, 2020 · 2 comments · Fixed by #900
Closed

Ex: 1.51 in Cryptol Textbook #887

manleykm opened this issue Sep 11, 2020 · 2 comments · Fixed by #900
Assignees
Labels
docs LaTeX, markdown, literate haskell, or in-REPL documentation
Milestone

Comments

@manleykm
Copy link

image

When I follow this exercise, saving the file with the function

twoPlusXY (x, y) = 2 + xy
    where xy = x * y

I get the type twoPlusXY : {a} (Ring a, Literal 2 a) => (a, a) -> a. However, the book says that I should be getting the type twoPlusXY : {a} (a >= 2, fin a) => ([a],[a]) -> [a]. I was told that this might be a change in Cryptol from 2.8 to 2.9.

@manleykm
Copy link
Author

Also, Exercise 1.54 asks "What is the value of all f [] for an arbitrary function f? Is this reasonable?". But the answer key gives the value of "any f []", changing the result from True to False.

@manleykm
Copy link
Author

Actually, it looks like the answers to 1.54 and 1.55 were just mixed up a little.

1.54 asks about "all f []", but gives the answer to "any f []".
1.55 asks about "any f []", but mentions "If we pass all an empty sequence, then we will always get False" (where it should be saying "If we pass any an empty sequence, then we will always get False").

@brianhuffman brianhuffman added the docs LaTeX, markdown, literate haskell, or in-REPL documentation label Sep 11, 2020
@atomb atomb added this to the 2.10.0 milestone Sep 22, 2020
@brianhuffman brianhuffman self-assigned this Sep 23, 2020
brianhuffman pushed a commit that referenced this issue Sep 23, 2020
This fixes an issue mentioned in a comment to #887.
@brianhuffman brianhuffman linked a pull request Sep 23, 2020 that will close this issue
brianhuffman pushed a commit that referenced this issue Sep 23, 2020
This fixes an issue mentioned in a comment to #887.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
docs LaTeX, markdown, literate haskell, or in-REPL documentation
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants