Re: [isabelle] even/odd with primrec
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"
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?
Simply because it wasn't designed to handle it. As there is no formal
notion of "rather simple looking function", primrec uses a fixed
syntactic scheme with exactly one function per mutually-recursive datatype.
For everything else use the function package, replacing the "primrec"
keyword with "fun".
This archive was generated by a fusion of
Pipermail (Mailman edition) and