-
Notifications
You must be signed in to change notification settings - Fork 302
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
First exercise too advanced? #960
Comments
That's a very fair point. If you'd like to submit a PR making the proposed change, I'll be happy to merge it. |
It is a good point. Looking back, I see the last change I made at a request from a reader made things harder rather than easier. In my view, the best way forward is to say either more or less. More:
Or less by deleting the paragraph at the end of the exercise, and accepting any form of answer. I lean toward the latter. |
I came here with the same issue; I'm not quite sure how best to update this, since if you start putting ...OK, gave it a try below. |
The very first exercise in the book asks the reader to write code before any of the syntax has been presented:
Intuitively, reading the question, my answer would have been (suc (suc (suc (suc (suc (suc (suc zero))))))), but the next sentences then ask for a type signature and explain how to reload the code in Emacs. This makes me think that I do need to write code after all.
Since the reader does not yet know how to write Agda definitions this may cause some frustration (it certainly did for me).
An educational way of fixing this might be this:
The text was updated successfully, but these errors were encountered: