Open ComFreek opened 3 years ago
?OuterTheory/InnerTheory1
, since that is the actual name of the theory. ?OuterTheory?InnerTheory1
is the URI coresponding to the declaration in ?OuterTheory
that corresponds to the nested theory, which - as a declaration - is not technically a theory at all. It might be that it still works as syntactic sugar, but in my opinion it shouldn't. Would be interesting to see what happens if there are some actual constants in InnerTheory1
and whether they're even available in InnerTheory2
if you include the declaration.
Either way ?InnerTheory1
alone should not work, since there's no theory by that name - but there could be one (outside of ?OuterTheory
), which it would refer to if that existed.Thanks. --> added documentation label: document how inclusions and nested modules have in a StackExchange Q&A
The issue on meta keys is still open.
I've never specified relative to what the keys are resolved. I had a feeling that metadata might live in scopes somehow orthogonal to the rest, but I never followed up on that.
meta keys:
in includes: