Jiekai (Apr 23 2022 at 13:02): Jiekai (Apr 23 2022 at 13:02):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 xss are the same one. But I don't know how to do that.
Jiekai (Apr 23 2022 at 13:25):I see. In count the list is my custom list. After renaming the custom list, it works
Notification Bot (Apr 23 2022 at 13:25):Jiekai has marked this topic as resolved.
Last updated: Apr 19 2024 at 20:15 UTC