leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
164 stars 92 forks source link

Propositions and currying #116

Open DavidPratten opened 6 months ago

DavidPratten commented 6 months ago

Hi,

Working through the book and loving it. Thanks.

Quick question on https://github.com/leanprover/theorem_proving_in_lean4/blob/master/propositions_and_proofs.md

In the section Propositional Logic we have

So if we have p q r : Prop, the expression p → q → r reads "if p, then if q, then r." This is just the "curried" form of p ∧ q → r.

I'm curious where the conjunction came from? Would it be possible to clarify the idea here?

I'm wondering if p → q → r is also the curried form of p ∨ q → r?

David