blanchette / logical_verification_2023 Goto Github PK

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"

First off, thank you for the amazing book. I found a typo in Section 12.6. Summary of New Lean Constructs (Page 173 of 2023 Standard Edition, August 22, 2023). The last two lines of the Constant subsection:

The explanations should be flipped. Hope this helps.