Re: [isabelle] Problem with overloading and inductive



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?

Christoph





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