Search Results
| Search type | Search syntax |
|---|---|
| Tags | [tag] |
| Exact | "words here" |
| Author |
user:1234 user:me (yours) |
| Score |
score:3 (3+) score:0 (none) |
| Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
| Views | views:250 |
| Code | code:"if (foo != bar)" |
| Sections |
title:apples body:"apples oranges" |
| URL | url:"*.example.com" |
| Saves | in:saves |
| Status |
closed:yes duplicate:no migrated:no wiki:no |
| Types |
is:question is:answer |
| Exclude |
-[tag] -apples |
| For more details on advanced search visit our help page | |
Results tagged with lean
Search options questions only
not deleted
user 122
Lean is a theorem prover and programming language, based on the calculus of constructions with inductive types. For version-specific questions, also add the [lean3] or [lean4] tags.
27
votes
4
answers
2k
views
How usable is Lean for constructive mathematics?
In my answer explaining the differences between Lean and Coq, I emphasized that Lean is "essentially classical" mostly due to sociological norms. … How usable is the Lean standard library (in Lean 3 or Lean 4) for doing non-HoTT constructive mathematics? …
- 9,195
2
votes
1
answer
174
views
Is type checking in "Ideal Lean" computably enumerable?
There are actually two type theoretic foundations of Lean given in Mario Carneiro's master's thesis. … While that is true for the algorithmic definitional equality version of Lean (which is honestly probably the version people mean when they ask questions about Lean), it isn't clear it holds of the more …
- 9,195
8
votes
0
answers
244
views
What would a fully classical and fully univalent ITP and library look like?
Lean has some features which conflict with UA. It might be that some such Lean features would be sorely missed, or maybe UA would provide good replacements. … The Lean version of LEM would remain the same but the Lean version of AC would have to be weakened. One can only state the proposition that there exists a choice function. …
- 9,195