doc: clarify how Lean supports constructive logic#110
Closed
chabulhwi wants to merge 4 commits into
Closed
Conversation
chabulhwi
force-pushed
the
bulhwi/clarify-text
branch
from
7556820 to
b9ebf5e
Compare
eric-wieser
reviewed
Apr 7, 2024
chabulhwi
force-pushed
the
bulhwi/clarify-text
branch
from
b9ebf5e to
703203b
Compare
Author
|
@eric-wieser I added a cautionary note for constructivists to Chapter Introduction. |
chabulhwi
force-pushed
the
bulhwi/clarify-text
branch
4 times, most recently
from
8cb6bf9 to
5010474
Compare
chabulhwi
force-pushed
the
bulhwi/clarify-text
branch
4 times, most recently
from
3db6016 to
913c9b8
Compare
The paragraph I added 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]. [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>
This note may help constructivists thinking of using Lean to save time.
> …, regardless of how simple the change may be. Jireh Loreaux said that the above phrasing ["seemed unnecessarily antagonistic."][0] I'd say it sounded 'highly critical' of the Lean core team but was also [pretty accurate.][1] Nevertheless, Siddhartha Gadgil and others in the Lean community seemed to [agree with Jireh Loreaux][2]. So I decided to remove it and the word "any" in the part "nor do they accept any changes." [0]: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/constructive.20tactic.20mode.20in.20lean/near/431770413 [1]: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/constructive.20tactic.20mode.20in.20lean/near/431789933 [2]: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/constructive.20tactic.20mode.20in.20lean/near/431787322
This change will make it easier for constructivists thinking of using Lean to locate the cautionary note for them.
chabulhwi
force-pushed
the
bulhwi/clarify-text
branch
from
913c9b8 to
a87ed72
Compare
Author
|
I'll close this pull request since #117 will revise the text. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The paragraph I added to Section 'Historical and Philosophical Context'
explains how Lean core supports constructive logic, whether the
Lean core team will provide tactics for constructive logic or accept
them from contributors, and whether a user can develop them by
oneself outside the core.
I also added a cautionary note for constructivists to Chapter
'Introduction.'
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