Minor corrections in Part 1 (Basics) of the book

[paulch42]

The page numbers refer to the non-tablet version of the book.

• p viii: the versions of Lean and math lib need to be updated (though perhaps it would be better to omit the versions to save having to remember to update here each time)
• p x: it states that hovering over a symbol then pressing Cmd or Ctrl shows the ascii versions; on my Mac I see the ascii versions just by hovering over, no need for the Cmd key
• p 3, last para before 1.1: spurious closing parenthesis after 'higher-order logic'
• p 28, 2nd para, after goal: 'Te' should be 'The'
• p 30, 2nd para: I think '?anything' might be intended, but just noting it in case you just meant 'anything'
• p 42, para after theorem: 'implication' should be 'equivalence'
• p 47: App': there are two instances of a subtype missing the '{' and '}'
• p 47, 2nd para of 4.7: ".. not only the two .." should be ".. not only do the two .."
• p 48, theorem case_5: "fix x : \tau" should be "fix x : \sigma"