[isabelle-dev] Nominal and FinFuns from the AFP

[Makarius]

On Thu, 31 May 2012, Brian Huffman wrote:

> On Thu, May 31, 2012 at 1:36 PM, Makarius <makarius at sketis.net> wrote:
>> On Thu, 31 May 2012, Andreas Lochbihler wrote:
>>
>>>> At some point, when I have bundles ready to work with the existing
>>>> notation commands, we can fine-tune this scheme further, to allow users
>>>> to
>>>> 'include' syntax in local situations.
>>>
>>> I tried to implement the new syntax for FinFuns with bundles and Brian's
>>> notation attribute
>>> (https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-April/002585.html),
>>> but it was not satisfactory.
>>
>>
>> I did not have time yet to look more closely at that.
>>
>> Note that notation is based on "syntax declarations" of the local theory
>> infrastructure, which is slightly different from what you have in
>> attributes.  So notation as attributes is a bad idea.
>
> Makarius:
>
> If you want to call one of my ideas a "bad idea", then I hope you have
> a better justification for this statement.

Formally, if you look what notation does, it is not like an attribute, but 
a syntax declaration.  This can be seen immediately in the sources.

What is not immediately visible is the long history around it, but quite a 
bit of it was discussed even on this mailing list in the past few years. 
Right now I don't have time to sort out the details, but I also don't want 
to waste time repeating mistakes from the past that are already known by 
the veterans on these mechanisms.

Anyway, there is nothing wrong with bad ideas.  Most of my own ideas are 
bad. One merely needs to sort them out and isolate the good ones from the 
many ideas that are floating around.


 	Makarius