Stream: Beginner Questions

Topic: Can I use a custom qualifier name?

view this post on Zulip Hernán Rajchert (May 04 2023 at 19:49):

Can I use a custom qualifier name when importing a theory?

I'm looking for something like

theory Scratch
  imports Very_Long_Name as foo
begin
 (* I want to use foo.xxx  *)
end

view this post on Zulip Manuel Eberl (May 05 2023 at 07:59):

Pretty sure that's not possible. What you can do is locally define custom notation using e.g. the notation command. Or abbreviation, but I think abbreviations are more difficult to get rid of again.

view this post on Zulip Wolfgang Jeltsch (May 05 2023 at 14:12):

There is also const_alias, although I cannot comment much on that, as I have never used it.

Last updated: Apr 27 2024 at 16:16 UTC