Qiyuan Xu (Jun 08 2021 at 11:14): Qiyuan Xu (Jun 08 2021 at 11:14):Update: I found it seems actaully easy to implement an attribute by Isar_Cmd.no_translations in src/Isar/isar_cmd.ML. I guess the problem could be solved quickly and apologize for the interruption.
Could a translation rule be disabled by an option like show_types?
Actually, I have a translation rule to conceal complicated detail that is not intended to be displayed to users, like this:
datatype 'a complicated = Complicated 'a
syntax omitted :: logic
translations "omitted" <= "CONST Complicated x"
term "Complicated x" (* displays "omitted :: 'a complicated" *)
Then I wish some way for my users, ideally an option, to disable this rule in order to have a look at the omitted detail.
I know the command no_translation, but I think it's not friendly for users, since, as far as I know, it requires giving the complete expression of the rule
no_translations "omitted" <= "CONST Complicated detail"
term "Complicated x" (* displays "Complicated x :: 'a complicated" *)
I really wish something like an option
declare[[some_option_to_show_omitted_detail = true]]
Any suggestions about this?
Last updated: Oct 31 2025 at 12:44 UTC