← Back to branch summary

~ubuntu-branches/ubuntu/vivid/agda-stdlib/vivid

« back to all changes in this revision

Viewing changes to src/Data/Unit.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (1.1.3)
  • Revision ID: package-import@ubuntu.com-20111129170035-00v3pq4mmhoo5ulf
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Unit.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
 
4
-- Some unit types
2
5
------------------------------------------------------------------------
3
6
 
4
7
module Data.Unit where
10
12
open import Relation.Binary.PropositionalEquality as PropEq
11
13
  using (_≡_; refl)
12
14
 
 
15
-- Some types and operations are defined in Data.Unit.Core.
 
16
 
 
17
open import Data.Unit.Core public
 
18
 
13
19
------------------------------------------------------------------------
 
20
-- A unit type defined as a record type
14
21
 
15
22
-- Note that the name of this type is "\top", not T.
16
23