Email Gateway (Aug 18 2026 at 14:39): Email Gateway (Aug 18 2026 at 14:39):From: Tobias Nipkow <nipkow@in.tum.de>
Hi everybody,
One of the most frequently used functions in HOL is "length". There are about
100,000 occurrences in the AFP. If you have ever used list extensively, you will
have wished that there was a shorthand. Here are two alternatives that come to mind:
"|xs|" is what mathematicians would write. However, it clashes with the ASCII
syntax for both records ("(|" and "|)") and iterated implications ("[|" and
|]"). The record syntax at least is in a bundle, but not the iterated
implication. Thus it requires additional spaces, eg "[ |xs| ]".
"len xs" is the obvious alphabetical shorthand.
If they ASCII syntaxes for [| etc were gone, alternative 1 would be my choice.
But wait that long? Why not have "len" tomorrow?
Thoughts?
Tobias
Email Gateway (Aug 18 2026 at 14:50):From: Makarius <makarius@sketis.net>
On 18/08/2026 16:38, Tobias Nipkow wrote:
One of the most frequently used functions in HOL is "length". There are about
100,000 occurrences in the AFP. If you have ever used list extensively, you
will have wished that there was a shorthand. Here are two alternatives that
come to mind:
- "len xs" is the obvious alphabetical shorthand.
I don't see why this should be a conclusive argument. The name "length" is
well-established, also in other languages of Isabelle (e.g. ML, Scala).
If they ASCII syntaxes for [| etc were gone, alternative 1 would be my choice.
But wait that long? Why not have "len" tomorrow?
Because we are between RC0 and RC1 of the coming release. Now is the time to
finish unfinished things, and not start new things.
Makarius
Email Gateway (Aug 19 2026 at 11:32):From: Tjark Weber <tjark.weber@it.uu.se>
On Tue, 2026-08-18 at 16:38 +0200, Tobias Nipkow wrote:
One of the most frequently used functions in HOL is "length". There
are about 100,000 occurrences in the AFP. If you have ever used list
extensively, you will have wished that there was a shorthand. [...]
- "len xs" is the obvious alphabetical shorthand.
It's just a name, of course. But length is descriptive and immediately
understandable, whereas len primarily optimizes for typing convenience.
Given that Isabelle/HOL has thousands of names, I'm not sure that
saving a few keystrokes is the consideration that should take priority.
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (Aug 19 2026 at 11:51):From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
On Wed, 19 Aug 2026 at 12:32, Tjark Weber <tjark.weber@it.uu.se> wrote:
On Tue, 2026-08-18 at 16:38 +0200, Tobias Nipkow wrote:
One of the most frequently used functions in HOL is "length". There
are about 100,000 occurrences in the AFP. If you have ever used list
extensively, you will have wished that there was a shorthand. [...]
- "len xs" is the obvious alphabetical shorthand.
It's just a name, of course. But length is descriptive and immediately
understandable, whereas len primarily optimizes for typing convenience.
Given that Isabelle/HOL has thousands of names, I'm not sure that
saving a few keystrokes is the consideration that should take priority.
Terseness is idolised in mathematical practice, even in some Isabelle
theory files, but many times it does not improve readability. As the
old software engineering dictum says, a notation should be easy to
read, not easy to write. Also, in the mathematical community plain
language is considered ambiguous, and to be avoided, but in this case
the name length conveys a straightforward meaning.
Last updated: Sep 02 2026 at 16:10 UTC