← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/Nat.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/Nat.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Natural numbers
3
5
------------------------------------------------------------------------
4
6
 
5
 
{-# OPTIONS --universe-polymorphism #-}
6
 
 
7
7
module Data.Nat where
8
8
 
9
9
open import Function
12
12
  using (Injection; module Injection)
13
13
open import Data.Sum
14
14
open import Data.Empty
15
 
open import Level using (zero)
 
15
import Level
16
16
open import Relation.Nullary
17
17
open import Relation.Binary
18
18
open import Relation.Binary.PropositionalEquality as PropEq
34
34
 
35
35
infix 4 _≤_ _<_ _≥_ _>_
36
36
 
37
 
data _≤_ : Rel ℕ zero where
 
37
data _≤_ : Rel ℕ Level.zero where
38
38
  z≤n : ∀ {n}                 → zero  ≤ n
39
39
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
40
40
 
41
 
_<_ : Rel ℕ zero
 
41
_<_ : Rel ℕ Level.zero
42
42
m < n = suc m ≤ n
43
43
 
44
 
_≥_ : Rel ℕ zero
 
44
_≥_ : Rel ℕ Level.zero
45
45
m ≥ n = n ≤ m
46
46
 
47
 
_>_ : Rel ℕ zero
 
47
_>_ : Rel ℕ Level.zero
48
48
m > n = n < m
49
49
 
50
50
-- The following, alternative definition of _≤_ is more suitable for
56
56
  ≤′-refl :                         m ≤′ m
57
57
  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n
58
58
 
59
 
_<′_ : Rel ℕ zero
 
59
_<′_ : Rel ℕ Level.zero
60
60
m <′ n = suc m ≤′ n
61
61
 
62
 
_≥′_ : Rel ℕ zero
 
62
_≥′_ : Rel ℕ Level.zero
63
63
m ≥′ n = n ≤′ m
64
64
 
65
 
_>′_ : Rel ℕ zero
 
65
_>′_ : Rel ℕ Level.zero
66
66
m >′ n = n <′ m
67
67
 
68
68
------------------------------------------------------------------------
166
166
-- A comparison view. Taken from "View from the left"
167
167
-- (McBride/McKinna); details may differ.
168
168
 
169
 
data Ordering : Rel ℕ zero where
 
169
data Ordering : Rel ℕ Level.zero where
170
170
  less    : ∀ m k → Ordering m (suc (m + k))
171
171
  equal   : ∀ m   → Ordering m m
172
172
  greater : ∀ m k → Ordering (suc (m + k)) m