Stream: Beginner Questions

Topic: Duplicate fact declaration during locale instantiation

Qiyuan Xu (Jan 01 2023 at 12:31):

Hello, dear friends,

I am instantiating a big locale that contains several small locales and some of the theorems in the small locales have the same name. Those theorems are just technical and not really used in the big locale, but they do cause an error during the instantiation, telling that 'Duplicate fact declaration is not allowed'.
So, is there any easy way to forget some lemmas in a locale or maybe suppress the declaration or maybe rename the confliction automatically?

Thank you, dear Isabelle's friends.

Jan van Brügge (Jan 01 2023 at 16:51):

If you wrote the code for the big locale, you can try to use hide_fact

Qiyuan Xu (Jan 02 2023 at 03:11):

hide_fact is not available in a locale context and cannot be used to hide a declaration in a locale. It only works for theory instead of local_theory at ML level.

Qiyuan Xu (Jan 02 2023 at 03:14):

Now I'm thinking locale quantifier is perhaps a conventional approach, though, it does not address the problem I asked.

Mathias Fleury (Jan 02 2023 at 06:55):

Even private does not allow to hide a lemma enough to avoid that problem

Last updated: Dec 21 2024 at 16:20 UTC