Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
avigad wants to merge 1 commit into
base: master
Choose a base branch
from
Open

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

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 3 additions & 4 deletions axioms_and_computation.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,10 +95,9 @@ computational interpretation. From a *classical* point of view, it is
more fruitful to maintain a separation of concerns: we can use one
language and body of methods to write computer programs, while
maintaining the freedom to use nonconstructive theories and methods
to reason about them. Lean is designed to support both of these
approaches. Core parts of the library are developed constructively,
but the system also provides support for carrying out classical
mathematical reasoning.
to reason about them. Although Lean's core logic is constructive,
Lean does not shy away from the use of classical reasoning in its
libraries and tactics.

Computationally, the purest part of dependent type theory avoids the
use of ``Prop`` entirely. Inductive types and dependent function types
Expand Down