Re: [isabelle] I need a meta-or

On 7/31/2013 3:29 PM, Makarius wrote:

Trueprop priority is 5, so dealing with the syntax of functions of type "prop => prop" and "prop => prop => prop" is tricky:

  Trueprop :: "bool => prop"   ("(_)" 5)

If you want to play with syntax, you can always use 'notation' and 'no_notation' to specify things in any way you like, but don't ask me about suitable priorities -- this is a black art and better not changed fundamentally.

Wanting to be a helpful, altruistic individual, I give you now a way to create some priority space, for that day when selfish indiviuals complain, moan, and groan about there not being enough space between the priorities of =>, !!, ==>, ==, and Trueprop, which are at 0, 0, 1, 2, and 5, you being well aware of such things.

For priorities 5 and above, you add 95 to them. This puts Trueprop at a nice 100. For priorities 0 to 4, you put them at 10, 20, 30, 40, and 50. That would be one way to do it, unless there's something I'm not considering.


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