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.

Sign up for GitHub

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

Jump to bottom

First exercise too advanced? #960

Open
Ninijura opened this issue Feb 6, 2024 · 3 comments · May be fixed by #986
Open

First exercise too advanced? #960

Ninijura opened this issue Feb 6, 2024 · 3 comments · May be fixed by #986

Comments

@Ninijura
Copy link
Contributor

Ninijura commented Feb 6, 2024

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
Copy link
Collaborator

wenkokke commented Feb 7, 2024

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
Copy link
Member

wadler commented Feb 8, 2024

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
Copy link

KevinDCarlson commented Apr 29, 2024 •
edited
Loading

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.

@KevinDCarlson KevinDCarlson linked a pull request Apr 29, 2024 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Suggested modification to first exercise KevinDCarlson/plfa.github.io
4 participants
@wenkokke @wadler @KevinDCarlson @Ninijura