← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/Product/Record.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-05-24 10:26:15 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110524102615-9tontf43bq9ym690
Tags: 0.5-1
http://bugs.debian.org/573807
http://bugs.debian.org/598708
* [9251e0b] Imported Upstream version 0.5
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [2c82171] Add watch file
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly
* [540ca3f] Improve short description
* [6b3e794] Add dependencies on compatible versions of the Agda library
* [7127678] Standards-Version bump to 3.9.2, no changes required
* [9d0ae30] Update to use ghc instead of ghc6
* [3f6879a] Set Maintainer to my d.o email address

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Product/Record.agda
1
 
------------------------------------------------------------------------
2
 
------------------------------------------------------------------------
3
 
 
4
 
{-# OPTIONS --universe-polymorphism #-}
5
 
 
6
 
 
7
 
module Data.Product.Record where
8
 
 
9
 
open import Data.Function
10
 
open import Level
11
 
 
12
 
infixr 4 _,_
13
 
infixr 2 _×_ _-×-_ _-,-_
14
 
 
15
 
------------------------------------------------------------------------
16
 
 
17
 
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
18
 
  constructor _,_
19
 
  field
20
 
    proj₁ : A
21
 
    proj₂ : B proj₁
22
 
 
23
 
open Σ public
24
 
 
25
 
_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
26
 
A × B = Σ A (λ _ → B)
27
 
 
28
 
------------------------------------------------------------------------
29
 
 
30
 
<_,_> : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ {x} → B x → Set c}
31
 
        (f : (x : A) → B x) → ((x : A) → C (f x)) →
32
 
        ((x : A) → Σ (B x) C)
33
 
< f , g > x = (f x , g x)
34
 
 
35
 
map : ∀ {a b p q}
36
 
        {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
37
 
      (f : A → B) → (∀ {x} → P x → Q (f x)) →
38
 
      Σ A P → Σ B Q
39
 
map f g = < f ∘ proj₁ , g ∘ proj₂ >
40
 
 
41
 
swap : ∀ {a b} {A : Set a} {B : Set b} → A × B → B × A
42
 
swap = < proj₂ , proj₁ >
43
 
 
44
 
_-×-_ : ∀ {a b i j} {A : Set a} {B : Set b} →
45
 
        (A → B → Set i) → (A → B → Set j) → (A → B → Set _)
46
 
f -×- g = f -[ _×_ ]- g
47
 
 
48
 
_-,-_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
49
 
        (A → B → C) → (A → B → D) → (A → B → C × D)
50
 
f -,- g = f -[ _,_ ]- g
51
 
 
52
 
curry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
53
 
        ((p : Σ A B) → C p) →
54
 
        ((x : A) → (y : B x) → C (x , y))
55
 
curry f x y = f (x , y)
56
 
 
57
 
uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
58
 
          ((x : A) → (y : B x) → C (x , y)) →
59
 
          ((p : Σ A B) → C p)
60
 
uncurry f p = f (proj₁ p) (proj₂ p)