WIP: co-de bruijn #12

Closed

rhi wants to merge 12 commits from 🥚🛁 into 🐉

rhi commented

2023-06-05 10:59:24 -04:00

Owner

👉 everybody's got to be somewhere (egtbs) (egg tubs)

pros:

always knowing when a name is used for sure, so that #11 and its ilk are fixed
(in the specific case of #11, the subst would be trimmed to just the vars used in the term, so the spurious i would go away)
equality checking get the dimensions trimmed for free

cons:

complexity
the efficiency from not having to shift de bruijn indices mentioned in the paper is irrelevant in the presence of delayed substitutions

👉 [everybody's got to be somewhere](https://arxiv.org/pdf/1807.04085v1.pdf) (egtbs) (egg tubs) pros: - always knowing when a name is used for sure, so that #11 and its ilk are fixed \ (in the specific case of #11, the subst would be trimmed to just the vars used in the term, so the spurious `i` would go away) - equality checking get the dimensions trimmed for free cons: - complexity - the efficiency from not having to shift de bruijn indices mentioned in the paper is irrelevant in the presence of delayed substitutions