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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and