Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] incompatible operand type

Email Gateway (Aug 19 2022 at 16:10):

From: M A <tesleft@hotmail.com>
Hi

when design a new unknown function max, it return incompatible operand type error, I tried add bracket, still got error, where is wrong?

lemma max_app [simp]: "((max xs) @ (max ys)) @ (max zs) = (max xs) @ ((max ys) @ (max zs))"

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

lemma max_app [simp]: "(max xs @ max ys) @ max zs = max xs @ (max ys @ max zs)"
apply(induct_tac xs)
apply(auto)
done

Regards,

Martin

Last updated: Apr 25 2024 at 04:18 UTC