Andrea Vezzosi (Jun 06 2023 at 08:12): Andrea Vezzosi (Jun 06 2023 at 08:12):Hi, is there a command to show the qualified name corresponding to a given unqualified one?
I have quite a few theories imported and it's not always easy to guess which one is bringing a name in scope.
Manuel Eberl (Jun 06 2023 at 12:07):I always use the following snippet:
ML_val ‹
@{term "int"}
›
I mostly use it to find out what actually lurks behind some custom syntax/notation or abbreviation.
Manuel Eberl (Jun 06 2023 at 12:08):For your use case, using the names_long option also works:
declare [[names_long]]
term int
Output:
"Int.int"
:: "Nat.nat ⇒ Int.int"
That's great, thanks!
Btw, is there a reference documentation for available options? Or a way to search for relevant ones?
Wolfgang Jeltsch (Jun 06 2023 at 23:03):As a first attempt, I’d suggest to look in the index of the Isabelle/Isar Reference Manual for entries that have “(attribute)” or “(antiquotation option)” at the end. Attributes and antiquotation options are not documented all at the same place in the reference manual, since they are documented where they belong topic-wise (e.g., simp_trace is documented in the section on the Simplifier).
Last updated: May 07 2024 at 01:07 UTC