# [isabelle] precedences and orderings

Dear Isabelle users,
I've been wondering how easy it is to implement, and how useful people
would find, a different mechanism for defining precedence: something
based on partial orderings instead of numerical values. (I believe that
the underlying representation is a search tree anyway...)
I'm thinking of something like:
consts "*" :: "N => N => N" (infixr [> "="])
consts "+" :: "N => N => N" (infixr [< "*", > "="])
consts "^" :: "N => N => N" (infixr [> "*"])
consts "++" :: "N => N => N" (infixr [= "+"])
where the [> "X"] makes the constant have greater precedence than X. [<
"X"], less than and [= "X"] equal to X. I think this would be a nicer
way to specify them... what do you think?
There is a little question as to the treatment of less well defined
situations, such as:
consts "a" :: "N => N => N" (infixr [> "="])
consts "b" :: "N => N => N" (infixr [> "a"])
consts "c" :: "N => N => N" (infixr [> "b"])
consts "x" :: "N => N => N" (infixr [< "c"])
in particular, how does "x" relate to "a" and "b"? I suggest that when
such ambiguity arises "x" would be given precedence equal to the nearest
element less than "c". Similarly for greater than: it could be
interpreted, when ambiguity arises, as 'just a little bigger than': the
same as the nearest next value.
Cycles should obviously produce errors. :)
Do any of you know of something like this in other systems? I do not
know much about parsing, so perhaps there is some reason why such
approaches are not implemented... ? (if so, I'd like to know!)
cheers,
lucas

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