[ add ] Data.Bool.contradiction fixing #2847

CHANGELOG.md

@@ -132,6 +132,11 @@ Additions to existing modules
   ```
   NB. the latter is based on `IsCommutativeRing`, with the former on `IsSemiring`.
 
+* In `Data.Bool`:
+  ```agda
+  contradiction : b ≡ true → b ≡ false → Whatever
+  ```
+
 * In `Data.Fin.Permutation.Components`:
   ```agda
   transpose[i,i,j]≡j  : (i j : Fin n) → transpose i i j ≡ j

src/Data/Bool.agda

@@ -8,6 +8,8 @@
 
 module Data.Bool where
 
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+
 ------------------------------------------------------------------------
 -- The boolean type and some operations
 
@@ -18,3 +20,9 @@ open import Data.Bool.Base public
 
 open import Data.Bool.Properties public
   using (T?; _≟_; _≤?_; _<?_)
+
+------------------------------------------------------------------------
+-- Other functions
+
+contradiction : ∀ {w} {Whatever : Set w} {b} → b ≡ true → b ≡ false → Whatever
+contradiction refl ()