First exercise too advanced?

[Ninijura]

The very first exercise in the book asks the reader to write code before any of the syntax has been presented:

Exercise seven (practice) {#seven}

Write out 7 in longhand.

-- Your code goes here

You will need to give both a type signature and definition for the variable seven. Type C-c C-l in Emacs to instruct Agda to re-load.

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:

-- seven : ℕ
-- seven = <Your code goes here>

Uncomment the code by removing the dashes and insert your definition.

[wenkokke]

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.

[wadler]

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:

seven : ? == 7
seven = refl

Or less by deleting the paragraph at the end of the exercise, and accepting any form of answer. I lean toward the latter.

[KevinDCarlson]

I came here with the same issue; I'm not quite sure how best to update this, since if you start putting ?s the user has to figure out how to handle those upon loading, while if you "accept" just any answer you're still stuck with the fact that the answer probably won't compile if the user doesn't know how to do a proper declaration.

...OK, gave it a try below.