← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Category/Monad/Indexed.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/Category/Monad/Indexed.agda
2
2
-- Indexed monads
3
3
------------------------------------------------------------------------
4
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
5
7
-- Note that currently the monad laws are not included here.
6
8
 
7
9
module Category.Monad.Indexed where
8
10
 
9
 
open import Data.Function
10
11
open import Category.Applicative.Indexed
 
12
open import Function
 
13
open import Level
11
14
 
12
 
record RawIMonad {I : Set} (M : IFun I) : Set₁ where
 
15
record RawIMonad {i f} {I : Set i} (M : IFun I f) :
 
16
                 Set (i ⊔ suc f) where
13
17
  infixl 1 _>>=_ _>>_
14
18
  infixr 1 _=<<_
15
19
 
34
38
 
35
39
  open RawIApplicative rawIApplicative public
36
40
 
37
 
record RawIMonadZero {I : Set} (M : IFun I) : Set₁ where
 
41
record RawIMonadZero {i f} {I : Set i} (M : IFun I f) :
 
42
                     Set (i ⊔ suc f) where
38
43
  field
39
44
    monad : RawIMonad M
40
45
    ∅     : ∀ {i j A} → M i j A
41
46
 
42
47
  open RawIMonad monad public
43
48
 
44
 
record RawIMonadPlus {I : Set} (M : IFun I) : Set₁ where
 
49
record RawIMonadPlus {i f} {I : Set i} (M : IFun I f) :
 
50
                     Set (i ⊔ suc f) where
45
51
  infixr 3 _∣_
46
52
  field
47
53
    monadZero : RawIMonadZero M