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.
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: Sep 25 2022 at 23:25 UTC