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

« back to all changes in this revision

Viewing changes to src/Algebra/Structures.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:
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Some algebraic structures (not packed up with sets, operations,
3
5
-- etc.)
4
6
------------------------------------------------------------------------
5
7
 
6
 
{-# OPTIONS --universe-polymorphism #-}
7
 
 
8
8
open import Relation.Binary
9
9
 
10
10
module Algebra.Structures where
12
12
import Algebra.FunctionProperties as FunctionProperties
13
13
open import Data.Product
14
14
open import Function
15
 
open import Level hiding (zero)
 
15
open import Level using (_⊔_)
16
16
import Relation.Binary.EqReasoning as EqR
17
17
 
18
18
open FunctionProperties using (Op₁; Op₂)