Deprecate inspect function in favour of new with ... in construct

[MatthewDaggitt]

@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.

[ajrouvoet]

I hope this would also (eventually) get rid of the imported [_] from PropositionalEquality which clashes with list singletons and others.

[MatthewDaggitt]

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.

[jamesmckinna]

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

[jamesmckinna]

The saga continues,unfortunately: agda/agda#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.

[jamesmckinna]

For v2.0: suggest removing the deprecation warning?

[MatthewDaggitt]

Opened a PR undeprecating it, and have moved this to Agda-future