tactic documentation

Stream: mathlib4

[Eric Wieser]

Yaël Dillies said:

Lean 4's haveI does not mean the same thing as Lean 3's haveI

Eric Wieser said:

Can you elaborate on this?

Ruben Van de Velde said:

It's now "I" for "inline" rather than "instance cache". I still don't know what that means in practice

Is there a linkifier like tactic4#haveI that would have told me that?

[Mario Carneiro]

sadly no, there is a docs4 linkifier but lean 4 tactic declaration names are not very guessable

[Eric Wieser]

Because there is nothing forcing them to live inside the tactic.interactive namespace like there was in Lean 3?

[Mario Carneiro]

Because they are not even named at all in many cases, the names are autogenerated

[Eric Wieser]

Do they have doc entries at all?

[Mario Carneiro]

they do

[Mario Carneiro]

the #help command will find them

[Eric Wieser]

Sorry, what I meant is, do those entries appear on docgen4?

[Mario Carneiro]

they do

[Mario Carneiro]

docs4#Std.Tactic.tacticHaveI_

[Eric Wieser]

It's unfortunate it doesn't show notation

[Mario Carneiro]

The raw output from #help might be a bit more helpful:

import Std
import Mathlib.Tactic.HelpCmd

#help tactic «haveI»

syntax "haveI"... [Std.Tactic.tacticHaveI_]
  `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term.

[Notification Bot]

12 messages were moved here from #mathlib4 > !4#2894 by Eric Wieser.

[Mario Carneiro]

unfortunately this also does not show the complete syntax declaration, it tries its best but the relevant data is not really in the environment

[Mario Carneiro]

but [Std.Tactic.tacticHaveI_] is clickable there so you can go to the declaration if you want to see it