Stream: Beginner Questions

Topic: Could a translation rule be disabled by an option?

view this post on Zulip 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: Aug 10 2022 at 20:22 UTC