It's gonna be one mofo of a mutual induction when I'm finished, I think, but I'm really quite optimistic about this tactic working. One of the three context zones in the main judgment has me a little mystified, however. I don't understand what it means, really. I just introduced it at one point to hold some variables that would have been free otherwise. I am compelled to hazily trust my intuition as to how to involve it in the proofs, but it seems to make everything go: it is the magic glue between the "outside world" and the variables of the unification problem.
It's gonna be one mofo of a mutual induction when I'm finished, I think, but I'm really quite optimistic about this tactic working. One of the three context zones in the main judgment has me a little mystified, however. I don't understand what it means, really. I just introduced it at one point to hold some variables that would have been free otherwise. I am compelled to hazily trust my intuition as to how to involve it in the proofs, but it seems to make everything go: it is the magic glue between the "outside world" and the variables of the unification problem.
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments
