agda
Deprecate `inspect` function in favour of new `with ... in` construct
@gallais added the inspect idiom as a first class language construct in Agda 2.6.2. We should consider using it in the library to simplify our code, and possibly deprecating the old inspect function to encourage other people to migrate as well.
I hope this would also (eventually) get rid of the imported [_] from PropositionalEquality which clashes with list singletons and others.
You're not the only one who has expressed this wish, @jamesmckinna also mentioned this. It will be deprecated first, but yes eventually it'll be removed.
Suggest closing this now, after the merge of #1930, notwithstanding the issues of strictness of inspect vs. laziness of with ... in ... raised by agda#5833
The saga continues,unfortunately: https://github.com/agda/agda/issues/6841 so, no, we should probably keep this open,even though the stdlib uses of inspect have been successfully massaged away, the deprecation itself might have to be reverted for the time being... sigh.