Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Variable names

Email Gateway (Aug 18 2022 at 10:08):

From: Tom Ridge <tjr22@cam.ac.uk>
Dear All,

We used to write e.g. (% v_. P v_)

But with recent development versions of Isabelle, it appears user
variable names are not allowed to end with an underscore. Can someone
confirm this? Would it be possible to lift this restriction? (We have
lots of code that would need to be updated to track this change.)

Thanks

Tom

Email Gateway (Aug 18 2022 at 10:08):

From: Makarius <makarius@sketis.net>
On Wed, 7 Feb 2007, Tom Ridge wrote:

We used to write e.g. (% v_. P v_)

But with recent development versions of Isabelle, it appears user
variable names are not allowed to end with an underscore.

Trailing underscore have been reserved for internal use many years ago,
although not all parts of the system have treated this uniformly.
Lambda-bound variables have been included in this general scheme recently,
motivated by a more serious treatment of %_. b where the body does not
mention the bound variable.

We have lots of code that would need to be updated to track this change.

You can add further decorations to prevent the last character being an
underscore, e.g. x_'

Makarius

Last updated: Nov 21 2024 at 12:39 UTC