mercredi 2 décembre 2020

If statement doesn't evaluate

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