avigad / lamr Goto Github PK

First of all, thank you very much @avigad for writing this textbook and making it publicly available for free! I'm very new to formal mathematics (and Lean in particular) and resources such as this one are crucially important for my learning experience!

While consulting this online textbook I've collected the following typos.

1. Introduction

Four centuries later, Lull's work resonated with Gottfied Gottfried Leibniz, [...]

2. Mathematical Background

The following item isn't displayed correctly (i.e. enumerated):

#. Prove by structural recursion that for any (extended) binary tree $t$, we have
$\fn{size}(t) \le 2^{\fn{depth}(t)} - 1$.

6. Decision Procedures for Propositional Logic

The function propagateWithNew is used to peform perform a split on the literal x.

7. Using SAT Solvers

the the same horizontal line, vertical line, or square. Below is one of the hardest sudoko sudoku puzzles with only 17 given numbers.

12. Decision Procedures for First-Order Logic

The first three rules express the reflexivity, symmmetry symmetry, and transitivity of equality,
respectively.

Hi,
End of second paragraph => repeating "the"
"the" the sum of the numbers up to i.