*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] [code func] attribute on overloaded definitions*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 08 May 2008 22:08:46 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <60E124F7-ACEE-4304-8C49-751C53875918@galois.com>*References*: <60E124F7-ACEE-4304-8C49-751C53875918@galois.com>*User-agent*: Thunderbird 2.0.0.9 (Macintosh/20071031)

Tobias John Matthews schrieb:

Hi, I am trying to generate executable code for some overloaded definitions: consts cplus :: "'a => 'b => 'b" defs (overloaded) cplus_nat_int_def[code func]: "cplus (a::nat) (b::int) == int a + b" cplus_int_nat_def[code func]: "cplus (a::int) (b::nat) == nat a + b" However, the code generator gives the following error: *** Type *** nat => int => int *** of defining equation *** "cplus ?a ?b == int ?a + ?b" *** is incompatible with declared function type *** ?'a::type => ?'b::type => ?'b::type *** At command "defs".What is the correct way to register code equations for overloadedfunctions?Thanks, -john

**References**:**[isabelle] [code func] attribute on overloaded definitions***From:*John Matthews

- Previous by Date: [isabelle] [code func] attribute on overloaded definitions
- Next by Date: [isabelle] Reasoning about k-fold cartesian products
- Previous by Thread: [isabelle] [code func] attribute on overloaded definitions
- Next by Thread: Re: [isabelle] [code func] attribute on overloaded definitions
- Cl-isabelle-users May 2008 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