Re: [isabelle] Problem with overloading and inductive
- To: Brian Huffman <brianh at cs.pdx.edu>
- Subject: Re: [isabelle] Problem with overloading and inductive
- From: c fe <zehfee at googlemail.com>
- Date: Mon, 2 Mar 2009 11:24:36 +0100
- Cc: isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org> <email@example.com>
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and