plfa
Describe need for step-≡ constructor in equational reasoning syntax
https://github.com/plfa/plfa.github.io/blob/dev/src/plfa/part1/Induction.lagda.md
It isn't clear that step-≡ within the following line is what imports what is being referred to as _≡⟨_⟩_ in the rest of the text:
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
I agree, it's not clear. How would you rewrite to make it clearer? If you submit a pull request I will consider it. I didn't explain more when I wrote it because I considered it a diversion, but clearly omitting an explanation got in the way of at least one reader, so I would consider new wording.
Apologies. I would ordinarily try to be more constructive and make a suggestion, but as I'm learning Agda from this material, I didn't actually understand what relationship step-≡ had to _≡⟨_⟩_ enough to hazard a guess until just now when I looked it up and realised Agda has an ability to add additional syntaxes for operators.
I'll try to put a PR up soonish. Not sure it'll hit the right note, but here's hoping!
I’m afraid that such a simple fix would still be confusing, but that a complete explanation would break up the flow of the text. I suggest that we acknowledge in the text that something strange is going on, and that _≡⟨_⟩_ is imported by its alias step-≡, and that we link to a separate page which goes into the details of Agda’s syntax macros and why we have to have step-≡ in the first place.
I don’t know whether we should write this explanation as a separate, unlisted “chapter”, or simply link to the documentation of syntax macros and the discussion—on a GitHub issue or in the CHANGELOG—of step-≡, but I would be leaning towards the former.
That is, I would recommend that we create a separate file…
src/plfa/notes/ReasoningSyntax.lagda.md
…in which we provide an overview of the problem, which we place in the appendix, and otherwise only link from this section and—later on—from the chapter on equality.
(Lifted from my response on the PR.)
This is related to #639 and #583, and as such I believe we should (1) use the version from the standard library in exercises, and (2) address it in the text as outlined in my comment linked above.
I think I'll close my PR then. I'm trying to be as helpful as possible, but I'd be more comfortable if someone better versed in this took a run at it.