← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Relation/Binary/StrictToNonStrict.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/Relation/Binary/StrictToNonStrict.agda
17
17
 
18
18
open import Relation.Nullary
19
19
open import Relation.Binary.Consequences
20
 
open import Data.Function
 
20
open import Function
21
21
open import Data.Product
22
22
open import Data.Sum
23
23
open import Data.Empty
49
49
  as (inj₂ x≈y) _          = x≈y
50
50
  as (inj₁ _)   (inj₂ y≈x) = Eq.sym y≈x
51
51
  as (inj₁ x<y) (inj₁ y<x) =
52
 
    ⊥-elim (trans∧irr⟶asym {≈ = _≈_} Eq.refl trans irrefl x<y y<x)
 
52
    ⊥-elim (trans∧irr⟶asym {_≈_ = _≈_} Eq.refl trans irrefl x<y y<x)
53
53
 
54
54
trans : IsEquivalence _≈_ → _<_ Respects₂ _≈_ →
55
55
        Transitive _<_ → Transitive _≤_