[Agda] hidden proofs
Liam O'Connor
liamoc at cse.unsw.edu.au
Tue Jul 30 19:46:07 CEST 2013
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
More information about the Agda
mailing list