← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/Nat/Divisibility.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/Divisibility.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Divisibility
3
5
------------------------------------------------------------------------
4
6
 
103
105
 
104
106
-- 0 only divides 0.
105
107
 
106
 
0∣0 : ∀ {n} → 0 ∣ n → n ≡ 0
107
 
0∣0 {n} 0∣n = P.antisym (n ∣0) 0∣n
 
108
0∣⇒≡0 : ∀ {n} → 0 ∣ n → n ≡ 0
 
109
0∣⇒≡0 {n} 0∣n = P.antisym (n ∣0) 0∣n
108
110
 
109
111
-- Only 1 divides 1.
110
112
 
111
 
1∣1 : ∀ {n} → n ∣ 1 → n ≡ 1
112
 
1∣1 {n} n∣1 = P.antisym n∣1 (1∣ n)
 
113
∣1⇒≡1 : ∀ {n} → n ∣ 1 → n ≡ 1
 
114
∣1⇒≡1 {n} n∣1 = P.antisym n∣1 (1∣ n)
113
115
 
114
116
-- If i divides m and n, then i divides their sum.
115
117
 
196
198
 
197
199
_∣?_ : Decidable _∣_
198
200
zero  ∣? zero                         = yes (0 ∣0)
199
 
zero  ∣? suc n                        = no ((λ ()) ∘′ 0∣0)
 
201
zero  ∣? suc n                        = no ((λ ()) ∘′ 0∣⇒≡0)
200
202
suc m ∣? n                            with n divMod suc m
201
203
suc m ∣? .(q * suc m)                 | result q zero    =
202
204
  yes $ divides q refl