Stream: Beginner Questions

Topic: ✔ Concrete Semantics ex 2.3


view this post on Zulip 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.

view this post on Zulip Jiekai (Apr 23 2022 at 13:25):

I see. In count the list is my custom list. After renaming the custom list, it works

view this post on Zulip Notification Bot (Apr 23 2022 at 13:25):

Jiekai has marked this topic as resolved.


Last updated: Aug 13 2022 at 06:26 UTC