search

bor0 / gidti

Book: Introduction to Dependent Types with Idris
https://leanpub.com/gidti
Other
76 stars 4 forks source link

Chapter 2: bound variables #24

Closed nbloomf closed 6 years ago

nbloomf commented 6 years ago

In section 2.3 on substitution, since quantifiers were introduced a few sections prior, I think it makes sense to talk about the difference between free and bound variables. (Since the audience may not have seen this before.)

bor0 commented 6 years ago

I think it will be a bit distracting. We already introduce these in 3.1.1, and your PR additionally polishes that part :)