Email Gateway (Aug 17 2022 at 13:28): Email Gateway (Aug 17 2022 at 13:28):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Nicole,
Most qualified names follow the default access policy. This is as
follows: a qualified name x1.---.xn.y can be accessed by any suffix of
the whole name, or by a prefix of x1.---.xn followed by y. Later
accesses take priority over earlier ones.
You are probably right in pointing out that accesses of names generated
by the datatype package (or by other packages) should always contain the
name of the datatype. This would also disable to refer by "splits" to
the splitting lemmas of the last datatype. I believe this hasn't been
considered a problem since traditionally theory names are upper case
while type names are lower.
Clemens
Last updated: May 03 2024 at 08:18 UTC