← Back to branch summary

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

« 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-12-30 20:02:46 UTC
  • mfrom: (1.1.4)
  • Revision ID: package-import@ubuntu.com-20111230200246-xl31fi4bnippohay
Tags: 0.6-1
* [a88bdc0] Imported Upstream version 0.6
* [7aea5f2] Update copyright for new copyright holders and for new DEP5

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Nat/Primality.agda
14
14
open import Relation.Nullary
15
15
open import Relation.Nullary.Decidable
16
16
open import Relation.Nullary.Negation
 
17
open import Relation.Unary
17
18
 
18
19
-- Definition of primality.
19
20
 
24
25
 
25
26
-- Decision procedure for primality.
26
27
 
27
 
prime? : ∀ n → Dec (Prime n)
 
28
prime? : Decidable Prime
28
29
prime? 0             = no λ()
29
30
prime? 1             = no λ()
30
31
prime? (suc (suc n)) = all? λ _ → ¬? (_ ∣? _)