← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/Nat.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/Data/Nat.agda
6
6
 
7
7
module Data.Nat where
8
8
 
9
 
open import Data.Function
10
 
open import Data.Function.Equality as F using (_⟨$⟩_)
11
 
open import Data.Function.Injection
 
9
open import Function
 
10
open import Function.Equality as F using (_⟨$⟩_)
 
11
open import Function.Injection
12
12
  using (Injection; module Injection)
13
13
open import Data.Sum
14
14
open import Data.Empty
52
52
 
53
53
infix 4 _≤′_ _<′_ _≥′_ _>′_
54
54
 
55
 
data _≤′_ : Rel ℕ zero where
56
 
  ≤′-refl : ∀ {n}                   → n ≤′ n
57
 
  ≤′-step : ∀ {m n} (m≤′n : m ≤′ n) → m ≤′ suc n
 
55
data _≤′_ (m : ℕ) : ℕ → Set where
 
56
  ≤′-refl :                         m ≤′ m
 
57
  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n
58
58
 
59
59
_<′_ : Rel ℕ zero
60
60
m <′ n = suc m ≤′ n
93
93
zero  + n = n
94
94
suc m + n = suc (m + n)
95
95
 
 
96
{-# BUILTIN NATPLUS _+_ #-}
 
97
 
96
98
-- Argument-swapping addition. Used by Data.Vec._⋎_.
97
99
 
98
100
_+⋎_ : ℕ → ℕ → ℕ
99
101
zero  +⋎ n = n
100
102
suc m +⋎ n = suc (n +⋎ m)
101
103
 
102
 
{-# BUILTIN NATPLUS _+_ #-}
103
 
 
104
104
_∸_ : ℕ → ℕ → ℕ
105
105
m     ∸ zero  = m
106
106
zero  ∸ suc n = zero
204
204
                  { isEquivalence = PropEq.isEquivalence
205
205
                  ; reflexive     = refl′
206
206
                  ; trans         = trans
207
 
                  ; ∼-resp-≈      = PropEq.resp₂ _≤_
208
207
                  }
209
208
              ; antisym  = antisym
210
209
              }
236
235
  ...                   | inj₂ n≤m = inj₂ (s≤s n≤m)
237
236
 
238
237
import Relation.Binary.PartialOrderReasoning as POR
239
 
module ≤-Reasoning = POR (DecTotalOrder.poset decTotalOrder)
240
 
  renaming (_≈⟨_⟩_ to _≡⟨_⟩_)
 
238
module ≤-Reasoning where
 
239
  open POR (DecTotalOrder.poset decTotalOrder) public
 
240
    renaming (_≈⟨_⟩_ to _≡⟨_⟩_)
 
241
 
 
242
  infixr 2 _<⟨_⟩_
 
243
 
 
244
  _<⟨_⟩_ : ∀ x {y z} → x < y → y IsRelatedTo z → suc x IsRelatedTo z
 
245
  x <⟨ x<y ⟩ y≤z = suc x ≤⟨ x<y ⟩ y≤z