The Coq mailing list

[chris jhons <chrisformal AT yahoo.co.uk>]

Dear all,

 

I want to define the following functions in Coq. Can you tell me how?

 

even :: nat -> bool

even 0 = true

even 1 = false

even (s (s n)) = even n

 

 

even' :: nat -> bool

odd   :: nat -> bool

even' 0 = true

even' (s n) = odd n

odd 0 = false

odd (s n) = even' n

 

Thanks.

 

Chris

---

 ALL-NEW 
Yahoo! Messenger 
- all new features - even more fun!