The true expert on this is, of course, Paul (now cc'd) but I think
that the short answer is that you cannot have two different binding
occurrences that are the same variable. That's just not how things
work. :(
In this case, I think you can probably just substitute in for the
variable, tho, in
I'm modelling dependent types in redex, and I've got a rule that looks like
this:
[
(WellFormed (EnvExt x gU Gamma))
(Check (EnvExt x gU Gamma) gu gV)
---
"CheckLamPi"
(Check Gamma (CanonicalLam x gu) (CanonicalPi x gU
2 matches
Mail list logo
