theorem_proving_in_lean4 icon indicating copy to clipboard operation
theorem_proving_in_lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

fix: clarify that Lean's core library uses classical logic

Open avigad opened this issue 9 months ago • 0 comments

This pull request responds to the request from Bulhwi Cha to clarify that Lean's core library is not committed to avoiding classical: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/constructive.20tactic.20mode.20in.20lean/near/431736331

The previous wording dates back to the early days of the Lean project and is no longer accurate.

avigad avatar May 27 '24 17:05 avigad