Re: [isabelle-dev] Preferred syntax for big GCD?

[Florian Haftmann]

Then let's got for capitalization.  See now 92680537201f.

Florian

Am 09.04.2016 um 22:05 schrieb Makarius:
> On Thu, 10 Mar 2016, Florian Haftmann wrote:
> 
>> in 66a381d3f88f, the usual syntax for big operators has been added for
>> GCD (and LCM):
>>
>>  (a) Gcd x \ A. f x
>>
>> An alternative could be
>>
>>  (b) GCD x \ A. f x
>>
>> The form (b) follows the tradition to have binders all-capitalized (SUP,
>> INF, UNION, INTER, THE, LEAST, SUM, PROD).
>>
>> On the other hand nearly all those binders have pretty symbolic syntax,
>> such that the all-capitalized variants rarely show up in theory text.
>> Since there is no generally accepted symbolic syntax for gcd, it might
>> be better to let the (slightly more readable) form (a) stand.
> 
> This thread is still open in current Isabelle/ef8d840f39fb.
> 
> As far as I can tell, the canonical form for binder-like syntax in ASCII
> is UPPERCASE.
> 
> I've recently made several rounds in replacing a lot of ASCII notation
> by Isabelle symbols, and thus can confirm that the situation of
> remaining ASCII usually follows that convention.
> 
> 
> Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-- 

PGP available:
http://isabelle.in.tum.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] Preferred syntax for big GCD?

[Makarius]

On Thu, 10 Mar 2016, Florian Haftmann wrote:


in 66a381d3f88f, the usual syntax for big operators has been added for
GCD (and LCM):

 (a) Gcd x \ A. f x

An alternative could be

 (b) GCD x \ A. f x

The form (b) follows the tradition to have binders all-capitalized (SUP,
INF, UNION, INTER, THE, LEAST, SUM, PROD).

On the other hand nearly all those binders have pretty symbolic syntax,
such that the all-capitalized variants rarely show up in theory text.
Since there is no generally accepted symbolic syntax for gcd, it might
be better to let the (slightly more readable) form (a) stand.


This thread is still open in current Isabelle/ef8d840f39fb.

As far as I can tell, the canonical form for binder-like syntax in ASCII 
is UPPERCASE.


I've recently made several rounds in replacing a lot of ASCII notation by 
Isabelle symbols, and thus can confirm that the situation of remaining 
ASCII usually follows that convention.



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

Re: [isabelle-dev] Preferred syntax for big GCD?

[Lawrence Paulson]

I’m sympathetic to this view. On the other hand, GCD is the only one of these 
uppercase formulations that’s actually in widespread use.
Larry

> On 10 Mar 2016, at 09:46, Florian Haftmann 
>  wrote:
> 
> Since there is no generally accepted symbolic syntax for gcd, it might
> be better to let the (slightly more readable) form (a) stand.
> 
> I have no strong opinion on this.  Any suggestions?

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

Re: [isabelle-dev] Preferred syntax for big GCD?

[Tobias Nipkow]

THE, LEAST, GCD.

Tobias

On 10/03/2016 10:46, Florian Haftmann wrote:

Hi all,

in 66a381d3f88f, the usual syntax for big operators has been added for
GCD (and LCM):

   (a) Gcd x \ A. f x

An alternative could be

   (b) GCD x \ A. f x

The form (b) follows the tradition to have binders all-capitalized (SUP,
INF, UNION, INTER, THE, LEAST, SUM, PROD).

On the other hand nearly all those binders have pretty symbolic syntax,
such that the all-capitalized variants rarely show up in theory text.
Since there is no generally accepted symbolic syntax for gcd, it might
be better to let the (slightly more readable) form (a) stand.

I have no strong opinion on this.  Any suggestions?

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

[isabelle-dev] Preferred syntax for big GCD?

[Florian Haftmann]

Hi all,

in 66a381d3f88f, the usual syntax for big operators has been added for
GCD (and LCM):

  (a) Gcd x \ A. f x

An alternative could be

  (b) GCD x \ A. f x

The form (b) follows the tradition to have binders all-capitalized (SUP,
INF, UNION, INTER, THE, LEAST, SUM, PROD).

On the other hand nearly all those binders have pretty symbolic syntax,
such that the all-capitalized variants rarely show up in theory text.
Since there is no generally accepted symbolic syntax for gcd, it might
be better to let the (slightly more readable) form (a) stand.

I have no strong opinion on this.  Any suggestions?

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.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