Re: [isabelle] Problem with overloading and inductive



Hi Christoph,

Your inductive specification fixes the argument type of each use of "lifu", but it doesn't specify what the return type is. Do you intend the equality comparison to be at type "nat", "int", or something else? This is why you get the message about an extra type variable.

You'll need to add extra type annotations, like this:

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

Hope this helps,

- Brian


Quoting c_feller <c_feller at informatik.uni-kl.de>:

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.