From c12118177685803f36e6584953232f4c00f3528e Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Fri, 19 Jun 2020 13:13:13 +0300
Subject: [PATCH] Function mapping `Not (x=True)` to `x=False` was added for
 `Bool`s (#322)

---
 libs/base/Data/Bool.idr           | 12 ++++++++++++
 tests/idris2/coverage010/expected |  2 +-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/libs/base/Data/Bool.idr b/libs/base/Data/Bool.idr
index a1b3902b9..ed2516026 100644
--- a/libs/base/Data/Bool.idr
+++ b/libs/base/Data/Bool.idr
@@ -97,3 +97,15 @@ export
 notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y
 notOrIsAnd False _ = Refl
 notOrIsAnd True  _ = Refl
+
+-- Interaction with typelevel `Not`
+
+export
+notTrueIsFalse : {1 x : Bool} -> Not (x = True) -> x = False
+notTrueIsFalse {x=False} _ = Refl
+notTrueIsFalse {x=True}  f = absurd $ f Refl
+
+export
+notFalseIsTrue : {1 x : Bool} -> Not (x = False) -> x = True
+notFalseIsTrue {x=True} _  = Refl
+notFalseIsTrue {x=False} f = absurd $ f Refl
diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected
index 07bbfe147..20cebab1e 100644
--- a/tests/idris2/coverage010/expected
+++ b/tests/idris2/coverage010/expected
@@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at:
 12	main : IO ()
 13	main = do
 
-	Calls non covering function Main.case block in 2101(587)
+	Calls non covering function Main.case block in 2101(617)