search

robrix / path

A lambda calculus to explore type-directed program synthesis.
BSD 3-Clause "New" or "Revised" License
84 stars 2 forks source link

Shadowed bindings are indistinguishable in the context #77

Open robrix opened 5 years ago

robrix commented 5 years ago

Shadowing a binding locally extends the context, but there are rules in e.g. Unifiers as Equivalences—Proof-Relevant Unification of Dependently Typed Data that require context extension to not re-bind names. We can deal with this by including lines/columns in local QNames.