Re: [isabelle] Problem with overloading and inductive

Hallo Brian,

On Sat, Feb 28, 2009 at 6:32 PM, Brian Huffman <brianh at> 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.


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