Quick question: Is it guaranteed that for any two
b such that
KerName.equal (Constant.canonical a) (Constant.canonical b), their bodies as looked up in
Environ.Global.view are the same?
Hm, no, they're going to be equal up to a kernel name substitution.
So, in particular equal up to the kernel "α-equivalence"
(which is way strong than conversion but still not literally structural equality)
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: Dec 01 2023 at 04:01 UTC