Open avigad opened 4 months ago
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.
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.