← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/Nat.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Nat.agda
8
8
 
9
9
open import Function
10
10
open import Function.Equality as F using (_⟨$⟩_)
11
 
open import Function.Injection
12
 
  using (Injection; module Injection)
 
11
open import Function.Injection using (_↣_)
13
12
open import Data.Sum
14
13
open import Data.Empty
15
14
import Level
16
15
open import Relation.Nullary
 
16
import Relation.Nullary.Decidable as Dec
17
17
open import Relation.Binary
18
18
open import Relation.Binary.PropositionalEquality as PropEq
19
19
  using (_≡_; refl)
28
28
  zero : ℕ
29
29
  suc  : (n : ℕ) → ℕ
30
30
 
31
 
{-# BUILTIN NATURAL ℕ    #-}
32
 
{-# BUILTIN ZERO    zero #-}
33
 
{-# BUILTIN SUC     suc  #-}
 
31
{-# BUILTIN NATURAL ℕ #-}
34
32
 
35
33
infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_
36
34
 
192
190
compare (suc .m)           (suc .m)           | equal   m   = equal   (suc m)
193
191
compare (suc .(suc m + k)) (suc .m)           | greater m k = greater (suc m) k
194
192
 
 
193
-- If there is an injection from a type to ℕ, then the type has
 
194
-- decidable equality.
195
195
 
196
 
eq? : ∀ {s₁ s₂} {S : Setoid s₁ s₂} →
197
 
      Injection S (PropEq.setoid ℕ) → Decidable (Setoid._≈_ S)
198
 
eq? inj x y with to ⟨$⟩ x ≟ to ⟨$⟩ y where open Injection inj
199
 
... | yes tox≡toy = yes (Injection.injective inj tox≡toy)
200
 
... | no  tox≢toy = no  (tox≢toy ∘ F.cong (Injection.to inj))
 
196
eq? : ∀ {a} {A : Set a} → A ↣ ℕ → Decidable {A = A} _≡_
 
197
eq? inj = Dec.via-injection inj _≟_
201
198
 
202
199
------------------------------------------------------------------------
203
200
-- Some properties