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

« back to all changes in this revision

Viewing changes to src/Category/Monad/Identity.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
* [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:
2
2
-- The identity monad
3
3
------------------------------------------------------------------------
4
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
5
7
module Category.Monad.Identity where
6
8
 
7
9
open import Category.Monad
8
10
 
9
 
Identity : Set → Set
 
11
Identity : ∀ {f} → Set f → Set f
10
12
Identity A = A
11
13
 
12
 
IdentityMonad : RawMonad Identity
 
14
IdentityMonad : ∀ {f} → RawMonad (Identity {f})
13
15
IdentityMonad = record
14
16
  { return = λ x → x
15
17
  ; _>>=_  = λ x f → f x