[isabelle-dev] {..n} and {..<n}
Brian Huffman
brianh at cs.pdx.edu
Sat Mar 7 16:10:58 CET 2009
"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
>
>
More information about the isabelle-dev
mailing list