I know that questions like these seem to be looked down upon, but I haven't been able to find answers on the internet. I have the following function:
fun count :: "'a ⇒ 'a list ⇒ nat" where
"count a [] = 0"
| "count a (b # xs) = (count a xs) + (if a = b then 1 else 0)"
It counts the number of elements in a list that match with the given item. Simple enough, however, when I do the following: value "count x [x,x,y,x,y]"
I get this as the output
"(if x = y then 1 else 0) + 1 + (if x = y then 1 else 0) + 1 + 1" :: "nat"
So you can see that there are hanging "if" statements and unevaluated additions in the output. Is it possible to make Isabelle simplify this?
Aucun commentaire:
Enregistrer un commentaire