Conversation
| -- | ||
| -- Explaining how to use the inspect idiom and elaborating on the way | ||
| -- it is implemented in the standard library. | ||
| -- This module is DEPRECATED. |
There was a problem hiding this comment.
Could we add a pointer towards the Agda documentation on the with idiom instead?
There was a problem hiding this comment.
Yes. I'd been going to add that, as previously, to the deprecation section of Relation.Binary.PropositionalEquality.Core, but happy to do so here too.
But NB. the upstream change will only arise in v2.9.0, but AFAIK, there aren't readthedocs pages for that release... yet... so there's a more annoying synchronisation problem, by contrast with #2931 / #2932
UPDATED: latest commit makes a forward-in-time pointer to the v2.9.0, assuming we sort out a sensible v2.4 release schedule for which this makes sense...
There was a problem hiding this comment.
Going back over #1930, I realised that I'd failed to push the claimed README.WithIn to explain the new syntax, on the model of the previous README.Inspect.
One thing to do might be to reinstate it as part of this PR, but I'd need to find it, and work out if it still makes sense against the new semantics!
Let me know whether you think this worthwhile before I push look for, never mind push, anything else!
3 participants
See recent discussion on #1580 . No
CHANGELOG.