Move properties of if_then_else_ from Haskell.Law to Haskell.Law.Bool

agda · Dec 19, 2023 · b8eaf97 · b8eaf97
1 parent fd2ca48
commit b8eaf97
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 10 deletions.
diff --git a/lib/Haskell/Law.agda b/lib/Haskell/Law.agda
@@ -3,12 +3,3 @@ module Haskell.Law where
 open import Haskell.Prim
 open import Haskell.Prim.Bool
 
-ifFlip : ∀ (b) (t e : a) → (if b then t else e) ≡ (if not b then e else t)
-ifFlip False _ _ = refl
-ifFlip True  _ _ = refl
-
-ifTrueEqThen : ∀ (b : Bool) {thn els : a} → b ≡ True → (if b then thn else els) ≡ thn
-ifTrueEqThen .True refl = refl
-
-ifFalseEqElse : ∀ (b : Bool) {thn els : a} → b ≡ False → (if b then thn else els) ≡ els
-ifFalseEqElse .False refl = refl
diff --git a/lib/Haskell/Law/Bool.agda b/lib/Haskell/Law/Bool.agda
@@ -61,3 +61,16 @@ not-not True = refl
 
 not-involution : ∀ (a b : Bool) → a ≡ not b → not a ≡ b
 not-involution .(not b) b refl = not-not b
+
+--------------------------------------------------
+-- if_then_else_
+
+ifFlip : ∀ (b) (t e : a) → (if b then t else e) ≡ (if not b then e else t)
+ifFlip False _ _ = refl
+ifFlip True  _ _ = refl
+
+ifTrueEqThen : ∀ (b : Bool) {thn els : a} → b ≡ True → (if b then thn else els) ≡ thn
+ifTrueEqThen .True refl = refl
+
+ifFalseEqElse : ∀ (b : Bool) {thn els : a} → b ≡ False → (if b then thn else els) ≡ els
+ifFalseEqElse .False refl = refl
diff --git a/lib/Haskell/Law/Ord/Maybe.agda b/lib/Haskell/Law/Ord/Maybe.agda
@@ -6,7 +6,6 @@ open import Haskell.Prim.Eq
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Ord
 
-open import Haskell.Law
 open import Haskell.Law.Bool
 open import Haskell.Law.Eq
 open import Haskell.Law.Equality hiding ( trustMe )