Errata
Errata for A Self-Verifying Theorem Prover.
Main errata
- Page 44. "This function provides a term level notion of equality, ..."
should be, "Much like the [equal] function provides a term level notion of
equality, ..."
- Page 65. Definition 8. Subsetp. The base case is T, not NIL.
Thanks to Dan Friedman for spotting the error!
- Page 104. let* is not imported.
- Page 161. Derived Rule 2. Right Expansion. The "given" formula should
be "A", not "A v B.". Thanks to Dan Connolly for spotting the error!
Typos spotted by Dan Friedman:
- Pg. 15: "and and" should be "and"
- Pg. 56 and 94: "))" should be ")))" in the basis step
- Pg. 84: "a a" should be "a"
- Pg. 151: Para 2: "then may" should be "then we may"
Misc. typos:
- Pg. 446. "and and" should be "and"
- Pg. 5. "that theorem prover" should be "that a theorem prover"
