← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« back to all changes in this revision

Viewing changes to src/Algebra/Operations.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [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

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra/Operations.agda
3
3
-- exponentiation)
4
4
------------------------------------------------------------------------
5
5
 
 
6
{-# OPTIONS --universe-polymorphism #-}
 
7
 
6
8
open import Algebra
7
9
 
8
 
module Algebra.Operations (s : Semiring) where
 
10
module Algebra.Operations {s₁ s₂} (S : Semiring s₁ s₂) where
9
11
 
10
 
open Semiring s hiding (zero)
 
12
open Semiring S hiding (zero)
11
13
open import Data.Nat using (zero; suc; ℕ)
12
 
open import Data.Function
 
14
open import Function
13
15
open import Relation.Binary
14
16
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
15
17
import Relation.Binary.EqReasoning as EqR