1
$\begingroup$

I find that Lean4 is rather hard to work to find keywords and related things. In coq the docs are pretty to search if I recall correctly. A quick search for Inductive send me to the grammer and lots of other grad docs about it: https://coq.inria.fr/doc/V8.19.0/refman/language/core/inductive.html?highlight=inductive#coq:cmd.Inductive

But say I want to write this code:

noncomputable def g (x : ℝ) : ℝ := 1 / x
#eval g 3 -- fails

and I want to evaluate it at a point where it is defined. But I get this error:

compiler IR check failed at '_eval', error: unknown declaration 'g'

but googling etc. doesn't help. I tried searching for the explanation of noncomputable but Google nor the Lean4 manual said anything useful e.g.,

enter image description here

No search results for 'noncomputable'.

Anyway, I'd like to find what noncomputable means and more importantly, the equivalent docs/manual that Coq has but in Lean4. Does that exist?

$\endgroup$
2
  • $\begingroup$ This is a great question and I hope you get a good answer, but I fear that you'll get the answer "Lean 4 is still pretty new and this is why the documentation is nowhere near as good as Coq's". In practice the way people learn how to use Lean quickly is by asking questions on the Lean Zulip, which is a highly active and very helpful research forum. I know that not everyone likes to work like this but right now it's by far the most efficient way to learn the technicalities of Lean. The problem with your code, by the way, is that the reals are a nonconcomputable object so #eval will never work. $\endgroup$ Feb 29 at 11:05
  • $\begingroup$ If there were an algorithm which could tell me whether a given real number was 0 or not then I could prove many new cases of the Birch and Swinnerton-Dyer conjecture, for example; the reals are necessarily noncomputable. You can prove g(3)=1/3 but that's a bit different. $\endgroup$ Feb 29 at 11:06

1 Answer 1

2
$\begingroup$

I don't know of a current place where all the keywords are defined. In particular, some keywords are used only once at in the first Lean file and other ones can be added on the fly. (For example, Mathlib adds lemma as a keyword I believe.)

If you hover over noncomputable, it sort of gives you more information, but it is sparse and the information is actually for irreducible_def. (I assume noncomputable is implemented as a macro which expands to irreducible_def or something like that.)

Introduces an irreducible definition. irreducible_def foo := 42 generates a constant foo : Nat as well as a theorem foo_def : foo = 42.

Similarly, there is #help command in Mathlib which lists all the commands and their documentation, but again noncomputable isn't there for some reason.

You may want to bring this up on the Lean Zulip.


As Kevin's comment says, Lean's documentation is clearly still lacking, and also there is a bit of an issue of non-centralized documentation. The Lean Manual (which people go to first) is very sparse and not a good resource overall. For this sort of thing, I think Theorem Proving in Lean is the best resource. If that doesn't work, there are other resources listed here, or you can ask here or on the Lean Zulip. (Zulip will probably get you a quicker answer, unfortunately.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.