Stream: Beginner Questions

Topic: Controlling visibility of theory content


view this post on Zulip Hanno Becker (Dec 05 2022 at 17:37):

Is there a way to control what part of a session/theory should be visible to other sessions?

view this post on Zulip Mathias Fleury (Dec 05 2022 at 17:49):

Kind of, you can hide lemmas, but it is slightly annoying, and find_thmstill sees them:

context
begin
private lemma myHiddenLemma: true
  sorry
end

view this post on Zulip Hanno Becker (Dec 05 2022 at 17:50):

Cool! Does this work for definitions, datatypes and type_synonyms as well?

view this post on Zulip Mathias Fleury (Dec 05 2022 at 17:52):

The other way is to use qualifiedwhich forces the user to write MyThy.LemmaName

view this post on Zulip Mathias Fleury (Dec 05 2022 at 17:54):

Hanno Becker said:

Cool! Does this work for definitions, datatypes and type_synonyms as well?

I don't remember, but I don't think so

view this post on Zulip Mathias Fleury (Dec 05 2022 at 17:56):

Actually according to grep, yes

view this post on Zulip Mathias Fleury (Dec 05 2022 at 17:57):

there are example for every command in the distribution (including one private datatypethat I have written :laughing: ) or in the AFP


Last updated: Mar 28 2024 at 20:16 UTC