search

math-comp / mcb

Mathematical Components (the Book)
Other
140 stars 25 forks source link

Chapter 5: typos + explanation on lambda-lifting + maximal insertion on Monoid.law #27

Closed gallais closed 7 years ago

gallais commented 7 years ago

Thanks! (I push-forced to keep a clean history. Looks like it got rid of your comment.)

anton-trunov commented 7 years ago

I still can see it, it's just behind the "Show outdated" link.

anton-trunov commented 7 years ago

If the book is aiming at mathematicians (as opposed to cs people) then I think "lambda-lifted" needs to be explained too. It seems that sect. 1.4 calls it "abstraction mechanism". By the way, "maximally inserted" occurs earlier in the book, but it isn't explained.

gares commented 7 years ago

Thanks for the fixes! I agree with @anton-trunov that lambda-lift is bit too CS oriented, but I see your point: the sentence needs to be more clear.

gares commented 7 years ago

Thanks!