Learning objectives. By the end of this chapter, read Prop as the
type of statements and a proof as an ordinary term, state natural
deduction’s introduction/elimination rules for ∧/∨/¬/→, write and
prove theorem/lemmas directly as terms, and reason about ∀/∃ and
equality via the anonymous constructor and rfl.
Sections
Prop: the type of statements- A recap of standard logic and logical calculus
theorem and lemma- Implication is a function type
- And, Or, Not
- Universal and existential quantifiers
- Equality reasoning
- Exercises