Logic and Proof

Stream: lean4

[Peter B]

Anyone know if (a) Is there a version of the CMU "Logic and Proof" book in Lean 4 rather than Lean 3, and if not (b) are there any guidelines about how best to mechanically translate proofs from 3 to 4?

[Peter B]

In fact...am I nuts, or is this book written in BOTH.

e.g., the examples in https://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html look like Lean 4 to me, but th examples in https://leanprover.github.io/logic_and_proof/classical_reasoning.html look like Lean 3. Am I wrong?

[Chris Bailey]

They're both lean 3.

[Chris Bailey]

I think mathport gets to your first question, but I don't think logic and proof would require something that heavy duty.

[Peter B]

Thank you!