## 2. Basics - Functional Programming in Lean eBook: [Chapter 2](https://www.engineering.upenn.edu/~cis5000/current/sf-lean/lf/html/Basics/#Basics) ### ## 2.2. Data and Functions eBook: [Chapter 2.2](https://www.engineering.upenn.edu/~cis5000/current/sf-lean/lf/html/Basics/#Logical-Foundations--Basics___-Functional-Programming-in-Lean--Data-and-Functions) #### 2.2.3 Booleans eBook: [Chapter 2.2.3](https://www.engineering.upenn.edu/~cis5000/current/sf-lean/lf/html/Basics/#Logical-Foundations--Basics___-Functional-Programming-in-Lean--Data-and-Functions--Booleans) LeanNotes snippets [[🧩 🧩 🧩 The characterizing lemmas of not, and, and or]] [[rfl-tactic|rfl]] 🧩 🧩 🧩 The LeanNotes coding style preview [[rewrite-tactic|rewrite]] - Generally, the [[LeanNotes coding style - Overview#Summary|LeanNotes coding style]] does not use the `rw` version. [[Ln-exact-show-tactic|exact-show]] 🧩 🧩 🧩 The nand' operation [[match-tactic|match]] [[infix-command|infix]] 🧩 🧩 🧩 and_true: the conjunctive right identity [[cases-tactic| cases]]