Stream: Coq users

Topic: Is Include not generative?


view this post on Zulip 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 *)

view this post on Zulip Pierre-Marie Pédrot (Sep 13 2020 at 17:36):

Include generates inductive aliases.

view this post on Zulip Pierre-Marie Pédrot (Sep 13 2020 at 17:37):

The same phenomenon happens for included axioms / parameters.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Sep 14 2020 at 09:42):

TFW I thought “bicephal” was once of your jokes and it isn’t.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2020 at 09:43):

If you prefer, it's the canonical-user duality

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 14 2020 at 09:51):

Anyway, thanks for confirming this is intended.


Last updated: Jan 28 2023 at 06:30 UTC