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

Quoting c fe <zehfee at googlemail.com>:

On Mon, Mar 2, 2009 at 12:31 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:[...] A possible workaround is to use abbreviations for type-specific instances. For example, if you have a lot of type annotations like "(lifu whatever :: nat)" in your theory, then you would probably benefit by making a nat-specific abbreviation, like this: [...]But why then use overloading in the first place? If I'm going to use lifu_nat from your example isn't it almost the same as declaring lifu and lifu_nat as seperate functions?

I'll give an example from the Isabelle libraries.

- Brian

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

**Re: [isabelle] Problem with overloading and inductive***From:*Brian Huffman

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

- Previous by Date: [isabelle] Extra type variables, type classes and locales
- Next by Date: [isabelle] Question about fun definitions and unfold
- Previous by Thread: Re: [isabelle] Problem with overloading and inductive
- Next by Thread: [isabelle] interpreters and continuations
- 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