*To*: c fe <zehfee at googlemail.com>*Subject*: Re: [isabelle] Problem with overloading and inductive*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 02 Mar 2009 03:31:45 -0800*Cc*: isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <a1e5e35a0903020224m87fd855oc315300e59d2b9c0@mail.gmail.com>*References*: <a1e5e35a0902270527t75860ad4k8620771e8256ca29@mail.gmail.com> <20090228093206.icxiz8l74csc0c44@webmail.pdx.edu> <a1e5e35a0903020224m87fd855oc315300e59d2b9c0@mail.gmail.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Quoting c fe <zehfee at googlemail.com>:

Thanks, that really helped. But it lead to me having to annotated quite a lot of expressions which made my terms look rather convoluted. And as I think that those terms are important I want them to look as comprehensible as possible. So I'm now back to different functions with the same mixfix syntax and keep getting ambiguous input warnings but the definitions look ok.

consts lifu :: "'a => 'b" abbreviation lifu_nat :: "'a => nat" where "lifu_nat == lifu" inductive ind_lifu :: "int list => int => bool" where base: "lifu_nat a = lifu_nat b ==> ind_lifu a b"

- Brian

**Follow-Ups**:**Re: [isabelle] Problem with overloading and inductive***From:*Dr. Brendan Patrick Mahony

**Re: [isabelle] Problem with overloading and inductive***From:*c fe

**References**:

- Previous by Date: Re: [isabelle] Problem with overloading and inductive
- Next by Date: Re: [isabelle] And mask
- Previous by Thread: Re: [isabelle] Problem with overloading and inductive
- Next by Thread: Re: [isabelle] Problem with overloading and inductive
- Cl-isabelle-users March 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