← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Data/M.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/M.agda
 
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
 
4
-- M-types (the dual of W-types)
 
5
------------------------------------------------------------------------
 
6
 
 
7
module Data.M where
 
8
 
 
9
open import Level
 
10
open import Coinduction
 
11
 
 
12
-- The family of M-types.
 
13
 
 
14
data M {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
 
15
  inf : (x : A) (f : B x → ∞ (M A B)) → M A B
 
16
 
 
17
-- Projections.
 
18
 
 
19
head : ∀ {a b} {A : Set a} {B : A → Set b} →
 
20
       M A B → A
 
21
head (inf x f) = x
 
22
 
 
23
tail : ∀ {a b} {A : Set a} {B : A → Set b} →
 
24
       (x : M A B) → B (head x) → M A B
 
25
tail (inf x f) b = ♭ (f b)