Lasse Blaauwbroek (Nov 17 2021 at 21:11): 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?
Pierre-Marie Pédrot (Nov 18 2021 at 07:22):Hm, no, they're going to be equal up to a kernel name substitution.
Pierre-Marie Pédrot (Nov 18 2021 at 07:23):So, in particular equal up to the kernel "α-equivalence"
Pierre-Marie Pédrot (Nov 18 2021 at 07:23):(which is way strong than conversion but still not literally structural equality)
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: Oct 08 2024 at 14:01 UTC