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

[Amine Chaieb]

Is it about removing the {..n} completely or just for SUM?

Amine.

Tobias Nipkow wrote:
> 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