Email Gateway (Aug 22 2022 at 12:08): Email Gateway (Aug 22 2022 at 12:08):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,
from the news file of Isabelle2016-RC1, one can see that the function internals are by default
now hidden, and only available if the functions are defined via [[function_internals]].
This is perfectly fine, however I encountered the problem that not ALL function internals are exposed,
e.g., when defining f, one sees both f_def and f_sumC_def as expected. However, at least in some formalization I also
need to access f_graph_def which is no longer made available, even if [[function_internals]] is enabled.
Is there any reason for always hiding _graph_def, or can it be made available again?
Cheers,
René
Email Gateway (Aug 22 2022 at 12:10):From: Makarius <makarius@sketis.net>
Internals follow the internal structure of packages, so this is not
"function_internals", but "inductive_internals".
Makarius
Email Gateway (Aug 22 2022 at 12:11):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Makarius,
thanks for the hint, it solved the problem.
According to the solution to my problem, I propose to change the NEWS-file accordingly.
Under the item for recursive function definitions where currently
only „function_internals“ is mentioned, it should also list „inductive_internals“, because
one has to activate both options to see the real internal definition of a function.
Just my opinion,
René
Last updated: Apr 25 2024 at 01:08 UTC