[isabelle] even/odd with primrec
we tried to define the functions even and odd like this:
primrec even :: "nat => bool"
and odd :: "nat => bool" where
"even 0 = True" |
"even (Suc n) = odd n" |
"odd 0 = False" |
"odd (Suc n) = even n"
and got the error
inconsistent functions for datatype "nat"
We suppose that this is due to the fact that we define a mutual
recursive primrec-function over a datatype (nat) that is not mutual
recursive. Is this true? Is there any not too technical explanation
why primrec cannot handle this rather simple looking function?
This archive was generated by a fusion of
Pipermail (Mailman edition) and