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 f46795a commit e3ba709Copy full SHA for e3ba709
CHANGELOG.md
@@ -242,7 +242,7 @@ Additions to existing modules
242
* In `Data.Bool.Properties`:
243
```agda
244
if-eta : ∀ b → (if b then x else x) ≡ x
245
- if-swap : ∀ b c → (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 : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
246
if-not : ∀ b → (if not b then x else y) ≡ (if b then y else x)
247
if-∧ : ∀ b → (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y)
248
if-∨ : ∀ b → (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y))
0 commit comments