Re: [isabelle] Problem with overloading and inductive



Hallo Brian,

On Sat, Feb 28, 2009 at 6:32 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:
> [...]
> You'll need to add extra type annotations, like this:
> [...]
> Hope this helps,
> [...]

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.

But thanks, nevertheless. I don't know how long I would have been
trying to solve this.

Greeting,
Christoph





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