search

math-comp / mcb

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

Fix minor typos in ch 3. #64

Closed pmundkur closed 6 years ago

pmundkur commented 6 years ago

This was a great chapter with nice explanations of the tactics.

ltnW, leq_subLR, addSnnS, leq_addl, leq_trans, mulSn, subnKC were used without definition, almost all in the last example. Also, the 'On the status of Axioms' seemed quite advanced for this early chapter, perhaps needs a star?