Re: [isabelle] LaTeXsugar



Another 2 of my cents (euro):

I worked quite a lot with sequences but never (consciously) encountered or used the notation from

  http://en.wikipedia.org/wiki/Sequence#Indexing

And in fact it seems quite misleading to me to use curly brackets (that have a strong association with sets) when dealing with ordered sequences.

cheers

chris


On 01/31/2013 07:17 AM, Tjark Weber wrote:
On Wed, 2013-01-30 at 22:16 +0100, Tobias Nipkow wrote:
Am 30/01/2013 14:53, schrieb Christian Sternagel:
On 01/30/2013 04:03 PM, Tobias Nipkow wrote:
I don't like the {f i|i. True} syntax either but your {f i}_i is a bit
non-standard, too, isn't it?
I don't know ;). I think {f i}_{i : ℕ} is fairly standard,

If you can convince me of that, I'll probably add your original syntax (unless
other problems crop up). I am just unsure myself, although it looks plausible.

I believe {f i}_{i : ℕ} is fairly standard to denote the *sequence* f 0,
f 1, f 2, ...; but it does not commonly denote the *set* {f i|i : ℕ}.
See, e.g., http://en.wikipedia.org/wiki/Sequence#Indexing

In my humble opinion, UN i. {f i} is the better solution. (Also, what
about range f?)

Best regards,
Tjark









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