Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "Full name" of a locale

view this post on Zulip Email Gateway (Aug 18 2022 at 15:57):

From: Steve W <s.wong.731@gmail.com>
Hi,

If I want to retrieve the full name of a locale in a theory (by
Sign.full_name?), how do I retrieve the binding? Why does Sign.full_name
need the binding?

Thanks in advance.

Steve

view this post on Zulip Email Gateway (Aug 18 2022 at 15:57):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Steve,

what you are looking for is Locale.intern.

Hope this helps,
Florian
signature.asc

Last updated: Apr 19 2024 at 08:19 UTC