idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity

Function mapping Not (x=True) to x=False was added for Bools (#322)

Browse Source
This commit is contained in:
Denis Buzdalov 2020-06-19 13:13:13 +03:00 committed by GitHub
parent da0e056d7e
commit c121181776
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 13 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libs/base/Data/Bool.idr
View File

@ -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

2
tests/idris2/coverage010/expected
View File

@ -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)