[isabelle] Problem with overloading and inductive



Hallo,

I have a problem when I try to use a overloaded function in a
inductive definition. I've made a small example to illustrate that:


consts lifu :: "'a => 'b"

overloading lifu1 == "lifu::'a list => int"
            lifu2 == "lifu::int => nat"
begin
definition lifu1 where "lifu1 == length"
definition lifu2 where "lifu2 == nat"
end

inductive ind_lifu :: "int list => int => bool"
where
base: "lifu (a::int list) = lifu (b::int) ==> ind_lifu a b"


If i try to give that to Isabelle/HOL, i get the message:

Specification depends on extra type variables: "'a::{}"

Did I do something wrong or is this a bug?

Thanks,
Christoph Feller





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.