← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Function.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/Function.agda
33
33
 
34
34
_∘_ : ∀ {a b c}
35
35
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
36
 
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
37
 
      ((x : A) → C (g x))
 
36
        (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
 
37
        ((x : A) → C (g x))
38
38
f ∘ g = λ x → f (g x)
39
39
 
40
40
_∘′_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
41
 
       (B → C) → (A → B) → (A → C)
 
41
         (B → C) → (A → B) → (A → C)
42
42
f ∘′ g = _∘_ f g
43
43
 
44
44
id : ∀ {a} {A : Set a} → A → A