Open oskgo opened 2 years ago
Adding to this, this feature would also allow for longer and more descriptive theory names, since they would not be kept short to make qualifications shorter anymore.
So, you already have the following syntax:
require [... as ...]
(Yes, the square brackets are part of the syntax). Could you check whether this implements your request? If so, I'll remove the square brackets from the syntax and close this issue.
What I don't like with the current mechanism is that if you import the same theory twice (with different names), then all symbols are duplicated (I'm not even sure that they are convertible):
require List [List as List2].
op foo := (++).
gives
more that one variable or constant matches `++'
the list of matching objects follows:
[operator]: Top.List.++ <#a>
[operator]: Top.List2.++ <#b>
I don't think this implements my request. I don't seem to be able to alias sub-theories, and not being able to identify the "alias" with the original would limit the usage when you're interacting with one of your transitive dependencies (This was the case in the example which made me make the request).
Implement syntax like
import ... as ...
for aliased theory imports.For example
import Bool.BoolFin as BF
should not give direct access toenumP
like a regular import would, but instead require the additional qualificationBF.enumP
. Essentially it would allow the user to writeBF
as a shorthand forBool.BoolFin
.Some deeply nested theories can get really long qualifiers. A regular import sometimes works (either of the theory itself or the theory it's contained in), but it's possible that existing identifiers become overloaded by the import.
This feature solves the problem by still requiring qualification, but giving the user more control over how to do it.