[Added Data.Nat.Primality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20111104153518
 Ignore-this: 67edbc4fd105034acb5cda7cb21bf9f
] addfile ./src/Data/Nat/Primality.agda
hunk ./src/Data/Nat/Primality.agda 1
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primality
+------------------------------------------------------------------------
+
+module Data.Nat.Primality where
+
+open import Data.Empty
+open import Data.Fin as Fin hiding (_+_)
+open import Data.Fin.Dec
+open import Data.Nat
+open import Data.Nat.Divisibility
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+open import Relation.Nullary.Negation
+
+-- Definition of primality.
+
+Prime : ℕ → Set
+Prime 0             = ⊥
+Prime 1             = ⊥
+Prime (suc (suc n)) = (i : Fin n) → ¬ (2 + Fin.toℕ i ∣ 2 + n)
+
+-- Decision procedure for primality.
+
+prime? : ∀ n → Dec (Prime n)
+prime? 0             = no λ()
+prime? 1             = no λ()
+prime? (suc (suc n)) = all? λ _ → ¬? (_ ∣? _)
+
+private
+
+  -- Example: 2 is prime.
+
+  2-is-prime : Prime 2
+  2-is-prime = from-yes (prime? 2)