On 07/10/2015 00:37, Michael Norrish wrote:
HOL4 and HOL Light both support the (sym) syntax to remove concrete syntax fixities. I
don't think HOL Light supports comments at this level. HOL4 does, using SML's (* ... *).
So, if you want to write the escaped *, you have to use our older
HOL4 and HOL Light both support the (sym) syntax to remove concrete syntax
fixities. I don't think HOL Light supports comments at this level. HOL4 does,
using SML's (* ... *). So, if you want to write the escaped *, you have to use
our older syntax for the same (using a $ for "op": $*), or
On Tue, 22 Sep 2015, Tobias Nipkow wrote:
The "op" noation is idiosyncratic, but there are examples (not in
individual formulae) where I find some such notation convenient. I would
welcome Haskell's "(+)", but that has a problem with "(*)". Unless we
can make that notation work, I don't think
>> Personally I would appreciate some move here, but this only makes sense
>> if we agree what the goal is and whether it is worth the effort.
> Unless we
> can make that notation work, I don't think we profit much by a change.
> Hence I am inclined to leave things as they are.
Ditto.
The "op" noation is idiosyncratic, but there are examples (not in individual
formulae) where I find some such notation convenient. I would welcome Haskell's
"(+)", but that has a problem with "(*)". Unless we can make that notation work,
I don't think we profit much by a change. Hence I am
The »op •« is infamous. Whatever you wish instead (my personal favorite
being no special syntax at all), problems include
a) to detect unintended printing behaviour
b) a suitable migration mechanisms
Concerning b), one you could imagine things like
a) alternative declarations (infix(l/r)_new
Is there a consensus that there is a problem with this notation? Having no
special syntax might work, especially with jEdit, where one can click on an
unexpected constant to see what it refers to.
Larry
> On 22 Sep 2015, at 15:21, Florian Haftmann
>
