avigad
commented
4 months ago @turibe @jdchristensen I apologize that it has taken me so long to find time to catch up on the PR and the discussion in #112. David is right that I am protective of things I have written, and I appreciate the sensitivity that both of you have shown. I have read over @turibe's proposed changes and they are generally very good. It's often hard to judge changes in isolation, but I plan to come back to TPIL soon to make revisions, so I think it makes sense to merge this PR as is, given that I'll have a chance to tinker with the text later.
jdchristensen
Suggestions to clarify some possibly confusing items. Main ones are:
Introducing arguments in a way consistent with the idea that functions really only take one argument at a time (currying); the current formulation might mislead the reader into thinking otherwise.
Expand the first apply tactic example, showing what gets unified and how the subgoals are generated.