Is it possible to improve this error or add a lint warning?

Stream: new members

[Dan Abramov]

I often make this mistake:

import Mathlib.Tactic

theorem foo (A B : Type) : ∃ f: B → A, ∀ a : A, ∃ b : B, f b = a := by
  let f (b: B) : A := sorry
  let g (a: A): B := sorry
  have hf : ∀ (a: A), f (g a) = a
  use f
  intro a
  use g a
  exact hf a

Can you spot what's wrong?

The error message says:

Screenshot 2025-09-06 at 22.35.34.png

That's ... strange. Here's another variation:

Screenshot 2025-09-06 at 22.36.52.png

What's wrong with this line?

Well, the problem is I forgot to give a value here:

have hf : ∀ (a: A), f (g a) = a

(This needs := something at the end.)

So I think it just tries to read the next lines as a continuation of that statement, and somehow it is able to keep going until use g a here becomes a type error:

  have hf : ∀ (a: A), f (g a) = a -- this is fine :/
  intro a -- this is also fine :/
  use g a -- finally not fine here

Why is it erroring so late? Is it possible to make it error much earlier? If multiline declarations like this are supported, is there any way to lint against what seems like unrelated tactic calls on next lines?

I don't understand why this works at all.

[Dan Abramov]

Ironically syntax highlighting on this site seems to better understand what's going on.

[Aaron Liu]

have without a value is a tactic which sets the value as a new goal and puts it at the front of the goal list

[Dan Abramov]

So it's like suffices but the other way around? I seriously think sometimes there's too many ways to do the same thing in Lean...

[Dan Abramov]

That does it explain it though, thanks.

[Ruben Van de Velde]

That syntax is deprecated though

[Dan Abramov]

Is it actively deprecated? I don't see warnings in the editor (like I do for say cc)

[Ruben Van de Velde]

Oh, maybe the deprecation is implemented as a mathlib linter. Maybe @Damiano Testa remembers

[Kyle Miller]

For what it's worth, this is a mathlib tactic. You can "go to definition" on it to check.

You can think of it as being a Lean 3 compatibility tactic, which made the porting easier. This was the only have back in Lean 3.

[Dan Abramov]

For what it's worth, this is a mathlib tactic

I see. I do understand the distinction, but it's confusing for me as a user. I think a lot of casual Lean users (and maybe non-casual too) don't differentiate "Lean tactic" from "Mathlib tactic", and many Lean users always import Mathlib anyway. Maybe it would be nice if hovering over a tactic said where it's defined (and offered something unique and googleable that helps me finds its docs). That's a tangent though.

[Dan Abramov]

Would it be possible to fully deprecate this version so that it showed squigglies for people importing Mathlib but not working on Mathlib itself?

[Kyle Miller]

Anything's possible, especially if someone volunteers to lead the charge :-)

Why do you need a googlable identifier if you can do go-to-definition? Mathlib doesn't have any docs for its have except for its docstring. Being able to use go-to-definition/go-to-declaration is a key skill when working with Lean, in my opinion.

Deprecating it will take work: evaluating how it's used, figuring out who uses it and what impact there will be (e.g. I think the natural number game uses it?), making it easy to migrate, communicating the deprecation, and also removing its use from mathlib.

Feel free to add context to the docstring that this is a mathlib-specific extension of have. I at least think that seems worth pointing out. If you do that, you should think about style so that this can be done uniformly for other such extensions. Or, there's submitting an issue to Lean core to show an import Mathlib.Tactic.Have line at the end of the hover, like for other definitions.

[Dan Abramov]

Not trying to add work on anyone's plate for now, just trying to understand how things are prioritized and how much work it is to move different parts of the mountain. :)

Why do you need a googlable identifier if you can do go-to-definition? Mathlib doesn't have any docs for its have except for its docstring. Being able to use go-to-definition/go-to-declaration is a key skill when working with Lean, in my opinion.

I think maybe this is a reasonable stance, but it wasn't obvious that this is the suggested approach to learn what each tactic or piece of syntax does. The reason it doesn't feel this way is because often clicking on the most common bits of syntax pulls you into the middle of implementation that is completely inscrutable to me as an end user. For example I click on if and see this:

Screenshot 2025-09-07 at 00.11.03.png

Is that supposed to be understandable to end user, or is there a place for a docstring here? I don't know. I click on apply and see this:

Screenshot 2025-09-07 at 00.11.56.png

Is this the entry point for learning what apply does? It doesn't feel so. I'm not even sure where to scroll to find the apply docstring. What about simp?

Screenshot 2025-09-07 at 00.12.46.png

The point I'm trying to make is that maybe "just click into definitions to learn what it is" can be a consistent stance, but then it needs to be paired with some way for go-to-definition to go to some reasonable "entry point" for that thing rather than deep into its internals. Alternatively, I would need a googleable identifier to learn what each piece of custom syntax is supposed to do (in the hope that documentation for it exists online).

I emphasize this because "how to learn what tactics do, what their list is, and how to use them" is IMO one of the biggest difficulties learning Lean. It can be solved in a noncomposable way (just give me a whole list on one website) but I hear that the desire is to embrace Lean's composition model so it's "self-documenting". Docstrings partially help. But sometimes they're very short and I really want a page with examples. I can't infer how each tactic is supposed to be used from the screenshots I posted above. If Lean "wants" me to learn about tactics by clicking into definitions, I think something is missing to direct me to the "right place" in those files.

[Dan Abramov]

Honestly a perfect place for "go to definition" to land might be some file that defines an entry point for the implementation (re-exported from its actual internals) along with a Lean sheet that shows example after example of how to use it. That's what I actually want to see when I "click into" a tactic.

[Dan Abramov]

It also doesn't help that the official documentation for tactics is super short. E.g. this is all it has to say about apply. Not a single example. How does one actually learn how to use it?

Screenshot 2025-09-07 at 00.21.17.png

The documentation really feels like it already assumes the reader is familiar with all these concepts and just serves to remind which of the concepts you already know each command represents.

I do understand docs are hard and no one has time to do them, etc, but I want to understand the intended direction. E.g. maybe the team thinks this is actually fine. Maybe the team thinks this is bad but nobody has time to fix them. Maybe the team thinks it should be solved in docstrings rather than on the site. Etc.

[Dan Abramov]

(I kind of went completely offtopic here so sorry about that! I also hear you re: complaining is cheap; for my part, for now, I'm writing some posts on by blog "in userland" as I don't feel like I have clear opinions on what should be done in docstrings or on the site yet. Getting a general vibe for what the team thinks can be helpful for me to form these opinions.)

[Kyle Miller]

My stance is just that "this is how I learned Lean", and I found it to be a very powerful feature that other languages rarely have — how often can you see where basic syntax is defined right from the IDE? Note that you need to know about "go to declaration" too; usually it's "go to declaration" that gives you the docstring and syntax definition. I mentioned both for a reason.

[Dan Abramov]

Oh yea I for sure love that it's available. I just think it's not enough to make Lean learnable and sometimes works against that (by making it seem inscrutable and removing the incentives to document stuff because more experienced users can fully learn by clicking).

I wasn't aware of "Go to Declaration" having a different behavior, thanks for highlighting that. Again — seems like a great power user feature but probably not the obvious way to learn the language unless it's written down somewhere that this is how one should learn it.

[Dan Abramov]

What do you think about the idea with "go to definition" going to a special file that has a re-export with a bunch of examples? I think this leans into (pardon the pun) the self-documenting approach while actually colocating the documentation (and making it clear where to add it). Is that feasible?

[Dan Abramov]

I guess currently the predominant style is "one file with many definitions" which would work against that Actually that's fine, the existing files can stay exactly as they are but "public" per-tactic files could be added that reexport stuff from internals.

[Kyle Miller]

I think the intended way to learn is to follow tutorials, read docstrings, reference the reference, etc.

The on-line help (using some very old terminology) is there to remind you how things work, or if you're browsing some mathlib code, it lets you know generally what things are for. These don't substitute for other references.

The Lean Language Reference isn't itself a tutorial. Certainly the apply tactic's description is light on details, but the reference is actively being worked on. The section you're looking at is automatically drawn directly from the docstrings I believe. You've observed how we in core try to improve docstrings as we have time and as we get feedback. For docstrings themselves there's a tough balance between "useful for reference" and "useful for learning", since you see the whole docstring every time you hover. The longer term goal is to have links from docstrings to fuller Lean Reference entries.

[Dan Abramov]

Right, I guess I feel like I would vastly prefer a file of concise examples (similar to what you see in TPIL) to just a docstring. Sort of as complementary runnable code you can actually inspect, as well as a way for maintainers to communicate what the intended use cases for each tactic are. This sort of works as a specification or a test too. Is this unreasonable? These could be pulled into the website automatically, similar to what happens with docstrings.

[Kyle Miller]

Dan Abramov said:

just trying to understand how things are prioritized

When it comes to mathlib, it's sort of meritocracy: anyone who has the time, ability, and energy and can find some maintainer who'll back the vision can get things done.

[Kyle Miller]

I'm not personally moved by the idea of "go to definition" going to runnable examples, but maybe in a future with docstring links there could be a link to a file; probably Mathlib could have a file in the tests directory, that way the examples are part of the test suite and you don't have to worry about whether they've gone out of sync?

[Dan Abramov]

I think that would be an improvement, yeah! Is linking to a file from a docstring already feasible or is there something technical missing for that?

[Kyle Miller]

That's something I don't know. One technical challenge that comes to mind is that you'd want the links to work within downstream projects too, so somehow it'd need to be a special URL scheme to open modules or other project files.

[Kyle Miller]

I got as far as learning that if there were a DocumentLinkProvider in the Lean VS Code extension for a lean-module scheme, then docstrings could contain links like lean-module://MathlibTest.HaveExamples. I don't know anything about how doable this is or if it could be on the roadmap.

[Dan Abramov]

Cool, thanks! I'm not "ready" to "really do things" yet but the itch is growing :)

[Damiano Testa]

Like Ruben, I also have a vague memory that this version of have-without-by was deprecated. However, maybe it was just a discussion on Zulip that did not make it into mathlib, or maybe a conclusion was not reached in the discussion.

[Damiano Testa]

Anyway, I am personally not a fan of this version of have and I avoid it when writing my own code.

[Damiano Testa]

Another possibility (which is probably not the case here), is that there could be a PR that is enforcing the deprecation, but it turned out that there were so many uses in mathlib, that the effort did not seem worth the gain.

[Ruben Van de Velde]

No, I'm 99% sure it is forbidden in mathlib already

[Ruben Van de Velde]

I'm thinking one of the mathlib.style linters

[Kevin Buzzard]

Dan Abramov said:

It also doesn't help that the official documentation for tactics is super short. E.g. this is all it has to say about apply. Not a single example. How does one actually learn how to use it?

My students at Imperial read the tactic documentation that comes with our course notes, e.g.
https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html

NB these detailed descriptions of basic tactics exist in our docs precisely because our students have been making the same observation as Dan for many years now.

[Kevin Buzzard]

I could add that I personally would not trust the reference manual to write anything which is comprehensible to beginner mathematicians. The docstring Dan quotes is a case in point. apply is a basic tactic which you need right at the start of your Lean journey. The quoted docstring is full of buzzwords that one does not learn until much later on (at least if one is a mathematician). And has no examples. Our documentation not only has examples but it contains an explicit warning about the misuse of the tactic which I have now seen literally hundreds of students attempt (i.e. using it as rw).

[Dan Abramov]

It doesn’t have to be this way! Reference manuals should be comprehensible to end users and should have examples. The problem with farming out basic examples to third-party courses is that those inevitably get stale and outdated.

[Dan Abramov]

Look at these docs:

• https://www.typescriptlang.org/docs/handbook/enums.html
• https://doc.rust-lang.org/stable/reference/items/enumerations.html
• https://learn.microsoft.com/en-us/dotnet/csharp/language-reference/builtin-types/enum
• https://learn.microsoft.com/en-us/dotnet/csharp/language-reference/language-specification/enums

All of these are first-party content and yet all of them provide clear examples and use accessible writing. I can understand these perfectly fine.

I think Lean reference needs to strive for a similar standard in writing. Clear, accessible, with examples.

[Dan Abramov]

In particular, https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html pretty much is what I’d expect rhe apply reference documentation to be. Not a single paragraph full of jargon.

[Dan Abramov]

Can we get some buy-in from the Lean maintainers to actually go ahead and do this? A page per tactic, each tactic has a clear description and a few examples. Who do we need to convince? I’m happy to write some pages myself if there’s a go-ahead.

[Dan Abramov]

cc @Jason Reed on above q

[Jason Reed]

Improving tactic documentation is something I've committed to for this coming quarter.

[Kevin Buzzard]

Oh that's great news! Jason -- see https://b-mehta.github.io/formalising-mathematics-notes/Part_2/Part_2.html for some battle-tested docs which you're welcome to take from without attribution (they're on Bhavik Mehta's page right now but he took over the course from me and as far as I know they're all just copied from my version https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2024/Part_C/Part_C.html which I wrote and as I say which you're welcome to use for inspiration or for anything else, if you want).

[Jason Reed]

Great, appreciate it!

[Kevin Buzzard]

In particular, students seemed to like the "summary/examples/details" set-up.

[Alfredo Moreira-Rosa]

I would say that if @Dan Abramov propose his help to write docs, you should take it. I think if i'm not mistaken, that dan lead the documentation team at meta for the React library. So he knows a litle bit about doc writing.

[Alfredo Moreira-Rosa]

And if i may add my two cents, i started learning lean using the natural game. This is a great way to start with lean.
I think i started beginning this year, but it took me this whole summer of vacation to dedicate some serious time to learning lean and reading the resources and starting being somewhat efficient at writing proofs.

For now, one of the most valuable resource for writing proofs (that you known how to prove by hand) is this cheat sheet :
https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf
So i think, something of the same kind should be included in the docs.