idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-27 13:40:15 +03:00
Code Issues Projects Releases Wiki Activity

Add orBothFalse proof

Browse Source
This commit is contained in:
Robert Wright 2023-06-30 15:16:19 +01:00 committed by G. Allais
parent af3c5fd454
commit 754f6af55c
1 changed files with 11 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -71,6 +71,17 @@ orNotTrue : (x : Bool) -> x || not x = True
orNotTrue False = Refl
orNotTrue True = Refl
export
orBothFalse : {0 x, y : Bool} -> (0 prf : x || y = False) -> (x = False, y = False)
orBothFalse prf = unerase $ orBothFalse' prf
where
unerase : (0 prf : (x = False, y = False)) -> (x = False, y = False)
unerase (p, q) = (irrelevantEq p, irrelevantEq q)
orBothFalse' : {x, y : Bool} -> x || y = False -> (x = False, y = False)
orBothFalse' {x = False} yFalse = (Refl, yFalse)
orBothFalse' {x = True} trueFalse = absurd trueFalse
-- interaction & De Morgan's laws
export