We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
style-guide
contradiction
⊥-elim
1 parent 08bc2b8 commit 54f5c38Copy full SHA for 54f5c38
doc/style-guide.md
@@ -717,3 +717,8 @@ used successfully in PR
717
systematic for `Nary` relations in PR
718
[#811](https://github.com/agda/agda-stdlib/pull/811)
719
720
+## Prefer use of `Relation.Nullary.Negation.Core.contradiction`
721
+
722
+Where possible use `contradiction` between two explicit arguments rather
723
+than appealing to the lower-level `Data.Empty.⊥-elim`. This provides
724
+clearer documentation for readers of the code.
0 commit comments