Remove needless dependencies using the new Agda option #2897
Description
Cf. agda/agda#8226
We should eventually run CI with this warning set to error out so as to avoid reintroducing
new needless dependencies.
{{ message }}
Cf. agda/agda#8226
We should eventually run CI with this warning set to error out so as to avoid reintroducing
new needless dependencies.