Skip to Content.
Sympa Menu

coq-club - [Coq-Club] even

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] even


chronological Thread 

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!


Archive powered by MhonArc 2.6.16.

Top of Page