We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 28241d8 commit f46795aCopy full SHA for f46795a
src/Data/Bool/Properties.agda
@@ -750,11 +750,12 @@ if-eta : ∀ b {x : A} →
750
if-eta false = refl
751
if-eta true = refl
752
753
-if-swap : ∀ b c {x y : A} →
754
- (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
755
-if-swap false _ = refl
756
-if-swap true false = refl
757
-if-swap true true = refl
+if-swap-else : ∀ b c {x y : A} →
+ (if b then x else (if c then x else y))
+ ≡ (if c then x else (if b then x else y))
+if-swap-else false _ = refl
+if-swap-else true false = refl
758
+if-swap-else true true = refl
759
760
if-not : ∀ b {x y : A} →
761
(if not b then x else y) ≡ (if b then y else x)
0 commit comments