I thought Include would behave generatively for modules, since it includes a copy of the included module. However, that seems restricted to functors, so my mental model of
Include is probably wrong; what's the right one? In particular, since two copies of the same inductive are distinct, what does
Include produce instead?
Module M1. Inductive MNat := O | S (_ : MNat). End M1. Module M2. Include M1. End M2. Variable n1 : M1.MNat. Let n2 : M2.MNat := n1. (* works! *) Fail Let n3 : M2.MNat2 := n1. (* indeed fails *)
Include generates inductive aliases.
The same phenomenon happens for included axioms / parameters.
It's a feature of the kernel that relies on a fragile system of bicephal names
TFW I thought “bicephal” was once of your jokes and it isn’t.
Well, it's not standard jargon but I don't think that what lurks in the kernel has an official name.
If you prefer, it's the canonical-user duality
the formal rules seem to have such a concept (abstractly). In a timestamp semantics, I guess the stamps would be copied.
Anyway, thanks for confirming this is intended.
Last updated: Jan 28 2023 at 06:30 UTC