[Agda] A proof of the irrationality of the square root in Agda

[Andreas Abel]

Just for the record, here is a picky comment.  A ring element p is prime if

   p | a*b  implies  p | a or p | b

The definition given below is the one of a irreducible element which is 
only divisible by itself and unit elements.

   http://en.wikipedia.org/wiki/Irreducible_element

For the ring of natural numbers, the two concepts are logically 
equivalent.  Thus, in number theory one uses the more popular term 
"primality" when speaking of irreducibility.

I do not know which concept Thierry is using in his proof...

Cheers,
Andreas

On 04.11.11 4:13 PM, Nils Anders Danielsson wrote:
> -- Definition of primality.
>
> Prime : ℕ → Set
> Prime 0 = ⊥
> Prime 1 = ⊥
> Prime (suc (suc n)) = (i : Fin n) → ¬ (2 + Fin.toℕ i ∣ 2 + n)


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/