Re: [isabelle] locales, including documentation & possible programming bugs
Thanks, Brian, that's very helpful! I was really confused by the
\equiv biz. Can you explain two more things:
what do the 1000 priorities here even mean: [1000,1000,1000,1000] 70?
If we right a b \cong c d, I want a & b to be bound really tightly
together, so 1000 sounds like a good number, and I want the whole
expression to be bound tighter than say and or implies, so 70 is a
good number. But then I'd write it as [1000, 70, 1000].
Rules stated in terms of object logic connectives, like "P \<and> Q
--> R", aren't very useful with the "rule" method. You had better
state rules using "==>", like
"P ==> Q ==> R" instead.
I've been puzzled for some time by the preference (especially in
Julien's Tarski geometry Coq code) by folks writing
P ==> Q ==> R ==> S ==> T ==> U
instead of the more sensible
P & Q & R & S & T ==> U .
And you're saying there's a good reason for this! Great! Can you
explain why the first approach works better with rules?
This archive was generated by a fusion of
Pipermail (Mailman edition) and