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 lean4
Search options not deleted
user 233
Lean 4 is the latest major version of the Lean theorem prover by Microsoft Research. Use this tag for questions specific to Lean 4; if it's about Lean in general, use the tag (lean).
5
votes
Accepted
How does one import Natural numbers in Lean 4 -- unknown identifier 'ℕ'?
They're there, they're just called Nat. If you want the abbreviation ℕ to work then you'll need a mathlib import e.g. import Mathlib.Data.Real.Basic will be fine. You can then right-click on the notat …
- 2,560
2
votes
What is the official way to reinstall Lean4 from scratch on a Mac or Linux?
I suspect (from your other question) that you're asking this because you believe you have things set up incorrectly, but hopefully my answer to your other question shows you that your set-up is fine a …
- 2,560
2
votes
Accepted
What am I doing wrong when proving the add_right_cancel theorem?
From
hd: a + d = b + d → a = b
h: a + d = b + d
Goal: a = b
you can use the apply tactic.
- 2,560
3
votes
Accepted
How does one create a lean project and have mathlib import work when not creating the lean p...
Your screenshot indicates that you are opening VS Code in $HOME. You need to open the root directory of the project folder instead. For example on the command line you need to run code . in the direct …
- 2,560
2
votes
Accepted
Type Theory Lean 3 to Lean 4
Some things changed but the type theory stayed exactly the same, so e.g. https://github.com/digama0/lean-type-theory/releases/tag/v1.0 is still a valid reference (edit: apparently this is not complete …
- 2,560