Re: [isabelle] LaTeXsugar



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.