*To*: c_feller <c_feller at informatik.uni-kl.de>*Subject*: Re: [isabelle] Problem with overloading and inductive*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Sat, 28 Feb 2009 09:32:06 -0800*Cc*: isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <a1e5e35a0902270527t75860ad4k8620771e8256ca29@mail.gmail.com>*References*: <a1e5e35a0902270527t75860ad4k8620771e8256ca29@mail.gmail.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Hi Christoph,

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

**References**:**[isabelle] Problem with overloading and inductive***From:*c_feller

- Previous by Date: Re: [isabelle] isatool problems
- Previous by Thread: [isabelle] Problem with overloading and inductive
- Next by Thread: [isabelle] Handling theory errors
- Cl-isabelle-users February 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list