[Added Data.Nat.Primality. Nils Anders Danielsson **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)