Re: [isabelle] precedences and orderings

I like your idea of defining precedence by partial ordering; I dislike the system of assigning numerical values as precedences, because this implies that you know the numerical precedences of all the other constants that have precedences, which I don't.

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

I do not agree to force "x" to relate to "a" and "b" if it does not. If ambiguity between "x" and "a" or "b" arises, then the parser should signal a parse error. This is less confusing, too, I think, because otherwise you have the old problem: What again was the nearest element less than "c"?? One should just accept that precedence is a partial ordering, not a total one.


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