search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

Deprecate existing definition of `⊥-elim` in favour of its irrelevant version `⊥-elim-irr` #2346

Open jamesmckinna opened 5 months ago

jamesmckinna commented 5 months ago 
          I further conjecture on #2329 that all uses of `⊥-elim` can be replaced by their irrelevant version `⊥-elim-irr`... so question for the maintainers, are we prepared to embrace such a (breaking?) change to the type of `⊥-elim`?

Originally posted by @jamesmckinna in https://github.com/agda/agda-stdlib/issues/2243#issuecomment-2021111222

This v3.0 issue concerns the breaking change not undertaken as part of #2243 .

With it, among other things, might go the unification (also breaking) of the types of contradiction and contradiction-irr in Relation.Nullary.Negation.Core and a more systematic treatment of 'computational irrelevance of negated propositions'... considered in #2199.