Clarification in Dafny tutorial

[RustanLeino]

What change in documentation do you suggest?

Feedback pass on from a student and her advisor:

[The student] started by working through the Dafny tutorial (https://dafny.org/dafny/OnlineTutorial/guide). ...Two problems that she found awkward (and where I wasn’t sure what the intent was). In Exercise 3, we think the only acceptable precondition is requires false, but I was surprised at that, since it seems like a relatively advanced topic for that point in the tutorial. Is there something weaker there? Similarly, for Exercise 8, she observed that you could satisfy the prompt by simply relabeling a and b as b and c, but that doesn’t seem “simpler” as suggested by the prompt. If this is all working as intended, that’s perfectly fine.