← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Data/Bool/Properties.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Bool/Properties.agda
243
243
commutativeRing-xor-∧ : CommutativeRing _ _
244
244
commutativeRing-xor-∧ = commutativeRing
245
245
  where
246
 
  import Algebra.Props.BooleanAlgebra as BA
 
246
  import Algebra.Properties.BooleanAlgebra as BA
247
247
  open BA booleanAlgebra
248
248
  open XorRing _xor_ xor-is-ok
249
249
 
279
279
T-≡ {false} = equivalence (λ ())       (λ ())
280
280
T-≡ {true}  = equivalence (const refl) (const _)
281
281
 
 
282
T-not-≡ : ∀ {b} → T (not b) ⇔ b ≡ false
 
283
T-not-≡ {false} = equivalence (const refl) (const _)
 
284
T-not-≡ {true}  = equivalence (λ ())       (λ ())
 
285
 
282
286
T-∧ : ∀ {b₁ b₂} → T (b₁ ∧ b₂) ⇔ (T b₁ × T b₂)
283
287
T-∧ {true}  {true}  = equivalence (const (_ , _)) (const _)
284
288
T-∧ {true}  {false} = equivalence (λ ())          proj₂
292
296
proof-irrelevance : ∀ {b} (p q : T b) → p ≡ q
293
297
proof-irrelevance {true}  _  _  = refl
294
298
proof-irrelevance {false} () ()
 
299
 
 
300
push-function-into-if :
 
301
  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) x {y z} →
 
302
  f (if x then y else z) ≡ (if x then f y else f z)
 
303
push-function-into-if _ true  = P.refl
 
304
push-function-into-if _ false = P.refl