Re: [isabelle] LaTeXsugar



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?)
Tjark almost convinced me and I will probably switch to UN i. {f i} in my development. The only reason why I still consider \{f i\}_i nice, is its brevity (but if it does not convey the intended meaning, there is no point using it).

Initially, I got the idea for \{f i\}_{i : I} (and derived \{f i\}_i) from the notation that is used for indexed families, see e.g.

  http://en.wikipedia.org/wiki/Indexed_family

But then, I was not aware that \{f i\}_{i : I} has a different meaning from \{f i | i : I\} (and in fact I'm pretty sure that I saw these notations used interchangeably, but can't put my finger on where).

cheers

chris








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