```
fun count :: "'a ⇒ 'a list ⇒ nat" where
"count t Nil = 0" |
"count t (Cons x xs) = (if t = x then (1 + (count t xs)) else count t xs)"
lemma count_less_than_length : "(count x xs) ≤ (length xs)"
```

In jEdit output

```
Type unification failed: Clash of types "_ list" and "_ list"
Type error in application: incompatible operand type
Operator: length :: ??'a list ⇒ nat
Operand: xs :: ??'b list
```

It seems that I need to state the two `xs`

s are the same one. But I don't know how to do that.

I see. In `count`

the list is my custom list. After renaming the custom list, it works

Jiekai has marked this topic as resolved.

Last updated: Dec 07 2023 at 20:16 UTC