Re: [isabelle] Variable names
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_'
This archive was generated by a fusion of
Pipermail (Mailman edition) and