<div>
<div>Hi Sergei,</div><div><br></div><div>I was pretty easily able to define "even" using a similar definition to your first one:</div><div><br></div><div>open import Data.Nat</div><div><br></div><div>mutual</div><div> data Even : ℕ → Set</div><div> where</div><div> even0 : Even 0</div><div> even-suc : {n : ℕ} → Even n → Even (suc (suc n)) </div><div><br></div><div>open import Relation.Nullary</div><div><br></div><div>even : (n : ℕ) -> Dec (Even n)</div><div>even zero = yes even0</div><div>even (suc zero) = no (λ ()) -- absurd pattern :)</div><div>even (suc (suc n)) with even n</div><div>... | yes p = yes (even-suc p)</div><div>... | no p = no (λ { (even-suc x) → p x })</div>
</div>
<div><div><br></div><div><br></div><div><br></div><div>If you wanted to include odd as well the proof is still possible, just a little longer.</div><div><br></div><div>Regards,</div><div>Liam</div><div><br></div></div>
<p style="color: #A0A0A8;">On Wednesday, 31 July 2013 at 3:33 AM, Sergei Meshveliani wrote:</p>
<blockquote type="cite" style="border-left-style:solid;border-width:1px;margin-left:0px;padding-left:10px;">
<span><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-size: 13px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; background-color: rgb(255, 255, 255); ">mutual</div><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-size: 13px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; background-color: rgb(255, 255, 255); ">data Even : ℕ → Set</div><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-size: 13px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; background-color: rgb(255, 255, 255); ">where</div><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-size: 13px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; background-color: rgb(255, 255, 255); ">even0 : Even 0</div><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-size: 13px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; background-color: rgb(255, 255, 255); ">even-suc : {n : ℕ} → Odd n → Even (suc n)</div><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-size: 13px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; background-color: rgb(255, 255, 255); "><br></div><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-size: 13px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; background-color: rgb(255, 255, 255); ">data Odd : ℕ → Set where</div><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-size: 13px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; background-color: rgb(255, 255, 255); ">odd-suc : {n : ℕ} → Even n → Odd (suc n)</div></span>
</blockquote>
<div>
<br>
</div>