Re: [isabelle] Follow-up [Re: Isabelle operator precedence]



Hi Tobias,

On 12-17, Tobias Nipkow wrote:
> You have prompted me to add a table of infix operators to the existing "What's
> in Main" manual (development version). In the process I have also fixed a few
> odd associativities, mostly making a few predicates non-associative. The table
> differs from yours in a number of respects. I am still debating if the framework
> operators like ==> should be in there too, although they come not from HOL but Pure.

Thanks for doing this! Looking at 
http://isabelle.in.tum.de/repos/isabelle/diff/0eaefd4306d7/src/Doc/Main/Main_Doc.thy and given that you asked for feedback (on Pure)
I'm wondering why they are ordered in this way (maybe the list 
is automatically generated which would be good from a
maintainability perspective), otherwise perhaps just order them
ascending or descending and perhaps add a sentence ``functions
always beat relations, relations always beat HOL logic symbols,
HOL logic symbols always beat Pure'' (maybe I'm oversimplifying ...)
If the list is autogenerated then just write that (so a reader
does not have to try to discover any meaning ...). Or briefly explain the 
other ordering principle you applied.

I'd also second Arthur that Pure would be nice to have too (unless
it is already elsewhere). In case sb knows it: user-defined functions 
are at 100 or 1000?

best,

-- 
Holger





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