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

On Mon, 12 Nov 2012, Holger Blasum wrote:

attached is an attempt to follow-up on last week's discussion (thanks!). I think it is good enough for myself at the moment, however in case sth like this would make it into user documentation note that there are still some gaps e.g. concerning precedence values e.g. of "set"/"list" type constructors or the application of user-defined functions.

Type => and \<lambda> is also "metalogic" in your categorisation, also the "::" notation for type and sort constraints. Isabelle/HOL re-uses the Pure type system for its purposes. Pure notation has rather low syntax priorities, which explains why it is all at the bottom of your list.


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