[isabelle-dev] {..n} and {..<n}

[Brian Huffman]

"SUM k<=i" is a bit more concise than "SUM k=0..i". Maybe one could be  
an abbreviation for the other, specifically for type nat? On the other  
hand, maybe it's not worth the extra confusion it might cause, and the  
difference in conciseness is not much.

Over all, it's probably better to just use "SUM k=0..i". I think this  
is closer to the standard mathematical notation anyway.

- Brian


Quoting Tobias Nipkow <nipkow at in.tum.de>:

> On nat, the sets {0..n} and {..n} are the same, which can be irksome.
> Hence I discourage the use of {..n}. However, there are notations such
> as "SUM k<=n. t" which stand for "setsum (%k. t) {..n}" and introduce
> {..n} by the backdoor.
>
> I am tempted to get rid of this and related notations and restrict to
> the canonical "SUM k=a..b. t".
>
> Would anybody miss the "k<=n" variant?
> Potential problem: for other types, eg int, k<=i cannot be replaced by
> some "k=a..i". But "SUM k<=i", "UN k<=i" over int (let alone real) seem
> unusual.
>
> Feelings?
>
> Tobias
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>