Module with properties of Bool was moved from contrib to base.

Author: buzden

libs/base/Data/Bool.idr

@@ -0,0 +1,82 @@
+module Data.Bool
+
+%access public export
+%default total
+
+notInvolutive : (x : Bool) -> not (not x) = x
+notInvolutive True  = Refl
+notInvolutive False = Refl
+
+-- AND
+
+andSameNeutral : (x : Bool) -> x && x = x
+andSameNeutral False = Refl
+andSameNeutral True = Refl
+
+andFalseFalse : (x : Bool) -> x && False = False
+andFalseFalse False = Refl
+andFalseFalse True = Refl
+
+andTrueNeutral : (x : Bool) -> x && True = x
+andTrueNeutral False = Refl
+andTrueNeutral True = Refl
+
+andAssociative : (x, y, z : Bool) -> x && (y && z) = (x && y) && z
+andAssociative True  _ _ = Refl
+andAssociative False _ _ = Refl
+
+andCommutative : (x, y : Bool) -> x && y = y && x
+andCommutative x True  = andTrueNeutral x
+andCommutative x False = andFalseFalse x
+
+andNotFalse : (x : Bool) -> x && not x = False
+andNotFalse False = Refl
+andNotFalse True = Refl
+
+-- OR
+
+orSameNeutral : (x : Bool) -> x || x = x
+orSameNeutral False = Refl
+orSameNeutral True = Refl
+
+orFalseNeutral : (x : Bool) -> x || False = x
+orFalseNeutral False = Refl
+orFalseNeutral True = Refl
+
+orTrueTrue : (x : Bool) -> x || True = True
+orTrueTrue False = Refl
+orTrueTrue True = Refl
+
+orAssociative : (x, y, z : Bool) -> x || (y || z) = (x || y) || z
+orAssociative True  _ _ = Refl
+orAssociative False _ _ = Refl
+
+orCommutative : (x, y : Bool) -> x || y = y || x
+orCommutative x True  = orTrueTrue x
+orCommutative x False = orFalseNeutral x
+
+orNotTrue : (x : Bool) -> x || not x = True
+orNotTrue False = Refl
+orNotTrue True = Refl
+
+-- interaction & De Morgan's laws
+
+orSameAndRightNeutral : (x, y : Bool) -> x || (x && y) = x
+orSameAndRightNeutral False _ = Refl
+orSameAndRightNeutral True  _ = Refl
+
+andDistribOrR : (x, y, z : Bool) -> x && (y || z) = (x && y) || (x && z)
+andDistribOrR False _ _ = Refl
+andDistribOrR True  _ _ = Refl
+
+orDistribAndR : (x, y, z : Bool) -> x || (y && z) = (x || y) && (x || z)
+orDistribAndR False _ _ = Refl
+orDistribAndR True  _ _ = Refl
+
+notAndIsOr : (x, y : Bool) -> not (x && y) = not x || not y
+notAndIsOr False _ = Refl
+notAndIsOr True  _ = Refl
+
+notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y
+notOrIsAnd False _ = Refl
+notOrIsAnd True  _ = Refl

libs/base/base.ipkg

@@ -16,6 +16,7 @@ modules = Control.Arrow
         , Control.Monad.Writer
 
         , Data.Bits
+        , Data.Bool
         , Data.Buffer
         , Data.Complex
         , Data.Erased

libs/contrib/Data/Bool/Extra.idr

@@ -1,82 +1,8 @@
+||| This is a backward-compatibility module.
+|||
+||| This module's original contents were moved to `Data.Bool`.
+||| It's okay to add something new to this module but it seems to be good
+||| to leave a public import of the `Data.Bool` module.
 module Data.Bool.Extra
 
-%access public export
-%default total
-
-notInvolutive : (x : Bool) -> not (not x) = x
-notInvolutive True  = Refl
-notInvolutive False = Refl
-
--- AND
-
-andSameNeutral : (x : Bool) -> x && x = x
-andSameNeutral False = Refl
-andSameNeutral True = Refl
-
-andFalseFalse : (x : Bool) -> x && False = False
-andFalseFalse False = Refl
-andFalseFalse True = Refl
-
-andTrueNeutral : (x : Bool) -> x && True = x
-andTrueNeutral False = Refl
-andTrueNeutral True = Refl
-
-andAssociative : (x, y, z : Bool) -> x && (y && z) = (x && y) && z
-andAssociative True  _ _ = Refl
-andAssociative False _ _ = Refl
-
-andCommutative : (x, y : Bool) -> x && y = y && x
-andCommutative x True  = andTrueNeutral x
-andCommutative x False = andFalseFalse x
-
-andNotFalse : (x : Bool) -> x && not x = False
-andNotFalse False = Refl
-andNotFalse True = Refl
-
--- OR
-
-orSameNeutral : (x : Bool) -> x || x = x
-orSameNeutral False = Refl
-orSameNeutral True = Refl
-
-orFalseNeutral : (x : Bool) -> x || False = x
-orFalseNeutral False = Refl
-orFalseNeutral True = Refl
-
-orTrueTrue : (x : Bool) -> x || True = True
-orTrueTrue False = Refl
-orTrueTrue True = Refl
-
-orAssociative : (x, y, z : Bool) -> x || (y || z) = (x || y) || z
-orAssociative True  _ _ = Refl
-orAssociative False _ _ = Refl
-
-orCommutative : (x, y : Bool) -> x || y = y || x
-orCommutative x True  = orTrueTrue x
-orCommutative x False = orFalseNeutral x
-
-orNotTrue : (x : Bool) -> x || not x = True
-orNotTrue False = Refl
-orNotTrue True = Refl
-
--- interaction & De Morgan's laws
-
-orSameAndRightNeutral : (x, y : Bool) -> x || (x && y) = x
-orSameAndRightNeutral False _ = Refl
-orSameAndRightNeutral True  _ = Refl
-
-andDistribOrR : (x, y, z : Bool) -> x && (y || z) = (x && y) || (x && z)
-andDistribOrR False _ _ = Refl
-andDistribOrR True  _ _ = Refl
-
-orDistribAndR : (x, y, z : Bool) -> x || (y && z) = (x || y) && (x || z)
-orDistribAndR False _ _ = Refl
-orDistribAndR True  _ _ = Refl
-
-notAndIsOr : (x, y : Bool) -> not (x && y) = not x || not y
-notAndIsOr False _ = Refl
-notAndIsOr True  _ = Refl
-
-notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y
-notOrIsAnd False _ = Refl
-notOrIsAnd True  _ = Refl
+import public Data.Bool

libs/contrib/Interfaces/Verified.idr

@@ -6,7 +6,7 @@ import Control.Algebra.NumericImplementations
 import Control.Algebra.VectorSpace
 import Data.Vect
 import Data.ZZ
-import Data.Bool.Extra
+import Data.Bool
 
 %default total
 %access public export

libs/contrib/Text/Lexer.idr

@@ -1,6 +1,6 @@
 module Text.Lexer
 
-import Data.Bool.Extra
+import Data.Bool
 
 import public Text.Lexer.Core
 import public Text.Quantity

libs/contrib/Text/Lexer/Core.idr

@@ -1,6 +1,6 @@
 module Text.Lexer.Core
 
-import Data.Bool.Extra
+import Data.Bool
 
 import public Control.Delayed