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

Error in Exercise 1.5 of "Programming in Cryptol" Textbook #873

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

Error in Exercise 1.5 of "Programming in Cryptol" Textbook #873

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

Comments

@manleykm
Copy link

manleykm commented Sep 1, 2020

Towards the top of page 10 in the "Programming in Cryptol" Textbook, there is an exercise which states:

Exercise 1.5. Compare the results of evaluating (5 : Z 7) + (6 : Z 7) with toInteger (5 : Z 7) + toInteger
(6 : Z 7) . What is the result of -3 : Z 7 ? Were the results what you expected?

However, entering 'toInteger (5 : Z 7) + toInteger (6 : Z 7)' into Cryptol results in the following error:

  Unsolvable constraints:
    • Integral (Z 7)
        arising from
        use of expression toInteger
        at <interactive>:1:23--1:32
    • Reason: Type 'Z 7' is not an integral type.

The textbook's answer manual at the end of the book claims that Cryptol should give an answer of 11.

@brianhuffman
Copy link
Contributor

It looks like this was broken when we rearranged the type classes for cryptol 2.9. These uses of toInteger will need to be changed to fromZ, which has the appropriate type.

@brianhuffman brianhuffman added the docs LaTeX, markdown, literate haskell, or in-REPL documentation label Sep 1, 2020
@brianhuffman
Copy link
Contributor

See also #613.

@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
@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
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