Paolo Giarrusso (Sep 13 2020 at 13:00): Paolo Giarrusso (Sep 13 2020 at 13:00):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.
Pierre-Marie Pédrot (Sep 13 2020 at 17:37):The same phenomenon happens for included axioms / parameters.
Pierre-Marie Pédrot (Sep 13 2020 at 17:37):It's a feature of the kernel that relies on a fragile system of bicephal names
Paolo Giarrusso (Sep 14 2020 at 09:42):TFW I thought “bicephal” was once of your jokes and it isn’t.
Pierre-Marie Pédrot (Sep 14 2020 at 09:43):Well, it's not standard jargon but I don't think that what lurks in the kernel has an official name.
Pierre-Marie Pédrot (Sep 14 2020 at 09:43):If you prefer, it's the canonical-user duality
Paolo Giarrusso (Sep 14 2020 at 09:51):the formal rules seem to have such a concept (abstractly). In a timestamp semantics, I guess the stamps would be copied.
Paolo Giarrusso (Sep 14 2020 at 09:51):Anyway, thanks for confirming this is intended.
Last updated: Sep 25 2023 at 12:01 UTC