Skip to content

Commit c8aa5ce

Browse files
committed
[add]: Data.Bool.Properties.if-swap-then
1 parent da8c66a commit c8aa5ce

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

CHANGELOG.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,7 @@ Additions to existing modules
242242
* In `Data.Bool.Properties`:
243243
```agda
244244
if-eta : ∀ b → (if b then x else x) ≡ x
245+
if-swap-then : ∀ b c → (if b then (if c then x else y) else y) ≡ (if c then (if b then x else y) else y)
245246
if-swap-else : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
246247
if-not : ∀ b → (if not b then x else y) ≡ (if b then y else x)
247248
if-∧ : ∀ b → (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y)

0 commit comments

Comments
 (0)