search

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

doc: clarify how Lean supports constructive logic #110

Closed chabulhwi closed 4 months ago

chabulhwi commented 7 months ago

The paragraph I added to Section 'Historical and Philosophical Context' explains how Lean core [supports constructive logic][0], whether the Lean core team will provide tactics for constructive logic or [accept them from contributors][1], and whether a user can [develop them by oneself][2] [outside the core][3].

I also added a cautionary note for constructivists to Chapter 'Introduction.'

[0]: https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/Movement.20from.20Std.20to.20Init/near/430339840 [1]: https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/How.20classical.20is.20std4.3F/near/383780177 [2]: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/constructive.20tactic.20mode.20in.20lean/near/431685357 [3]: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/constructive.20tactic.20mode.20in.20lean/near/431714863

Co-authored-by: Mario Carneiro di.gama@gmail.com Co-authored-by: Henrik Böving hargonix@gmail.com Co-authored-by: Kim Morrison kim@tqft.net

chabulhwi commented 7 months ago

@eric-wieser I added a cautionary note for constructivists to Chapter Introduction.

chabulhwi commented 4 months ago

I'll close this pull request since https://github.com/leanprover/theorem_proving_in_lean4/pull/117 will revise the text.