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"
base: "(lifu a :: nat) = (lifu b :: nat) ==> ind_lifu a b"

Hope this helps,

- Brian

Quoting c_feller <c_feller at>:


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"
definition lifu1 where "lifu1 == length"
definition lifu2 where "lifu2 == nat"

inductive ind_lifu :: "int list => int => bool"
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?

Christoph Feller

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