Stream: Beginner Questions

Topic: Renaming of context elements / types in locales

Carolos Lameris (Jun 06 2023 at 09:53):

Hello,

I was wondering whether when working in a pre-existing locale, whether it is possible to:
(i): Rename context elements.
(ii): Rename the type names of the context elements.

I would like to do so without creating a new locale.
The reason for this desire is to be able follow notation more closely when formalizing results from a particular text.

For example assume we have the following pre-existing locale.

locale ex_locale =
  fixes A B C

Here A, B & C are automatically given respective type names 'a, 'b & 'c.
I would like to rename the context elements A, B & C and the types 'a, 'b & 'c.

One way I have found to obtain the desired behavior is by defining a new "wrapper locale", where I rename the context elements and types:

locale ex_locale2 = ex_locale D E F
  for
    D :: "'d" and
    E :: "'e" and
    F :: "'f"

However this requires creating a new locale which I would prefer to avoid.
Is this possible?

Last updated: Apr 28 2024 at 04:17 UTC