Stream: Coq devs & plugin devs

Topic: Canonical vs User map


view this post on Zulip Lasse Blaauwbroek (Nov 17 2021 at 21:11):

Quick question: Is it guaranteed that for any two Constant.t's a and b such that KerName.equal (Constant.canonical a) (Constant.canonical b), their bodies as looked up in Environ.Global.view are the same?

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2021 at 07:22):

Hm, no, they're going to be equal up to a kernel name substitution.

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2021 at 07:23):

So, in particular equal up to the kernel "α-equivalence"

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2021 at 07:23):

(which is way strong than conversion but still not literally structural equality)

view this post on Zulip Lasse Blaauwbroek (Nov 18 2021 at 12:51):

Ah, okay. So does kernel name substitution approximately mean 'throw away all user representations from GlobRef's and keep only the canonical part'?


Last updated: Feb 05 2023 at 21:03 UTC