[Agda] hidden proofs

[Liam O'Connor]

Hi Sergei,

I was pretty easily able to define "even" using a similar definition to your first one:

open import Data.Nat

mutual
 data Even : ℕ → Set
  where
   even0 : Even 0
   even-suc : {n : ℕ} → Even n → Even (suc (suc n))  

open import Relation.Nullary

even : (n : ℕ) -> Dec (Even n)
even zero = yes even0
even (suc zero) = no (λ ()) -- absurd pattern :)
even (suc (suc n)) with even n
... | yes p = yes (even-suc p)
... | no p = no (λ { (even-suc x) → p x })




If you wanted to include odd as well the proof is still possible, just a little longer.

Regards,
Liam


On Wednesday, 31 July 2013 at 3:33 AM, Sergei Meshveliani wrote:

> mutual
> data Even : ℕ → Set
> where
> even0 : Even 0
> even-suc : {n : ℕ} → Odd n → Even (suc n)
>  
> data Odd : ℕ → Set where
> odd-suc : {n : ℕ} → Even n → Odd (suc n)


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130731/265a53f8/attachment.html