[isabelle] Extra type variables, type classes and locales
I have with a hidden extra type variable again and again I have no
clue what exactly went wrong. I've made a small example:
class testC = type +
fixes from_nat :: "nat => 'a"
and to_nat :: "'a => nat"
locale Test =
fixes dummy :: "'a::testC"
assumes dd: "ALL z::'a::testC. to_nat z ~= 0"
definition ftest :: "nat => 'a list" where "ftest n == [from_nat n]"
inductive test::"nat => nat => bool"
"((ftest a)::'a list) = ((ftest b)::'a list) ==> test a b"
I thought the locale not only fixed dummy but also 'a so that it isn't
necessarily an extra type variable in the inductive definition. Am I
wrong or is there another mistake in my example?
Thanks in advance,
This archive was generated by a fusion of
Pipermail (Mailman edition) and