Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Sean,
Is there a way to find out which types/constants/axioms are defined
just within
a particular theory? My (partial) understanding is as follows,
Sign.req_sg, Type.rep_tsig, etc gives you full information
about the types etc. that are currently in scope. So, the info
from, say,
Sign.rep_sg (theory "HOL")
are a subset of those of
Sign.rep_sg (theory "Set")
This understanding is sufficently right (the term "scope" is misleading
in this context, but that does not matter for the particular problem).
Is there an easy way, without looking at the theory file itself, to get
just the types etc. defined in, say, Set.thy?
Not a direct way, but you can achieve that by enumerating all constants
(type constructors, ...) in the current theory and from that set taking
away all constants (type constructors, ...) present in the ancestor
theories (see Theory.parents_of).
To get an idea how this may work, have a look at src/Pure/codegen.ML,
functions theory_of_const and thyname_of_const which show how this could
work in principle.
Hope this helps
Florian
signature.asc
Last updated: May 03 2024 at 12:27 UTC