← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to src/Data/Nat/Primality.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (2.1.4 sid)
  • Revision ID: package-import@ubuntu.com-20111129170035-be8cbok8ojft5tjl
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/Primality.agda
 
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
 
4
-- Primality
 
5
------------------------------------------------------------------------
 
6
 
 
7
module Data.Nat.Primality where
 
8
 
 
9
open import Data.Empty
 
10
open import Data.Fin as Fin hiding (_+_)
 
11
open import Data.Fin.Dec
 
12
open import Data.Nat
 
13
open import Data.Nat.Divisibility
 
14
open import Relation.Nullary
 
15
open import Relation.Nullary.Decidable
 
16
open import Relation.Nullary.Negation
 
17
 
 
18
-- Definition of primality.
 
19
 
 
20
Prime : ℕ → Set
 
21
Prime 0             = ⊥
 
22
Prime 1             = ⊥
 
23
Prime (suc (suc n)) = (i : Fin n) → ¬ (2 + Fin.toℕ i ∣ 2 + n)
 
24
 
 
25
-- Decision procedure for primality.
 
26
 
 
27
prime? : ∀ n → Dec (Prime n)
 
28
prime? 0             = no λ()
 
29
prime? 1             = no λ()
 
30
prime? (suc (suc n)) = all? λ _ → ¬? (_ ∣? _)
 
31
 
 
32
private
 
33
 
 
34
  -- Example: 2 is prime.
 
35
 
 
36
  2-is-prime : Prime 2
 
37
  2-is-prime = from-yes (prime? 2)