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

Tobias Nipkow nipkow at in.tum.de
Fri Mar 6 22:41:36 CET 2009

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



More information about the isabelle-dev mailing list