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.

Regards,
GB




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