Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

[Tobias Nipkow]

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 syntax for the same 
(using a $ for "op": $*), or you can just add spaces and write ( *), or ( * ).


Of course, "( * )" is ok. The only reason I have been a little wary of "(*)" is 
that people who are unaware of comments inside formulas would be totaly confused 
by the syntax error they get. But if your HOL4 experience suggests that this is 
not an issue, I would be in favour of "(sym)".


Tobias


Michael


On 6 Oct 2015, at 23:12, Makarius  wrote:

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 we profit much by a change. Hence I am 
inclined to leave things as they are.


"(*)" does not work, because it is in conflict with "(* comment *)" in inner syntax.  I have recently 
encountered a situation where it would have been better to replace inner comments by "-- ‹comment›", as known in outer 
syntax, but the double-minus was in conflict with some infix operators. The next idea was to replace "-- ‹comment›" by 
"— ‹comment›" with a newly introduced Isabelle symbol for the mdash.

So many clouds of dust, caused by trying to clean up obscure corners ...

At the moment I am also inclined to leave things unchanged.


   Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

[Michael Norrish]

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 you can just add 
spaces and write ( *), or ( * ).

Michael

> On 6 Oct 2015, at 23:12, Makarius  wrote:
>
> 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 we profit much by a change. Hence I am inclined 
>> to leave things as they are.
>
> "(*)" does not work, because it is in conflict with "(* comment *)" in inner 
> syntax.  I have recently encountered a situation where it would have been 
> better to replace inner comments by "-- ‹comment›", as known in outer syntax, 
> but the double-minus was in conflict with some infix operators. The next idea 
> was to replace "-- ‹comment›" by "— ‹comment›" with a newly introduced 
> Isabelle symbol for the mdash.
>
> So many clouds of dust, caused by trying to clean up obscure corners ...
>
> At the moment I am also inclined to leave things unchanged.
>
>
>   Makarius___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

[Makarius]

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 we profit much by a change. 
Hence I am inclined to leave things as they are.


"(*)" does not work, because it is in conflict with "(* comment *)" in 
inner syntax.  I have recently encountered a situation where it would have 
been better to replace inner comments by "-- ‹comment›", as known in outer 
syntax, but the double-minus was in conflict with some infix operators. 
The next idea was to replace "-- ‹comment›" by "— ‹comment›" with a newly 
introduced Isabelle symbol for the mdash.


So many clouds of dust, caused by trying to clean up obscure corners ...

At the moment I am also inclined to leave things unchanged.


Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

[Florian Haftmann]

>> 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.

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

[Tobias Nipkow]

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 inclined to leave things as 
they are.


Tobias

On 22/09/2015 16:21, Florian Haftmann wrote:

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 beside infix(l/r),
infix(l/r) beside infix(l/r)_old)
b) a flag to control the semantics of infix(l/r)
c) a flag combined with a data slot to modify existing mixfix
declarations afterwards also

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.

Cheers,
Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

[Larry Paulson]

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 
>  wrote:
> 
> 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 beside infix(l/r),
> infix(l/r) beside infix(l/r)_old)
> b) a flag to control the semantics of infix(l/r)
> c) a flag combined with a data slot to modify existing mixfix
> declarations afterwards also
> 
> 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.
> 
> Cheers,
>   Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev