Infoview in term mode

Stream: lean4

[Floris van Doorn]

The infoview is a great way to inspect the type of a theorem, especially when the pretty printer hides some information that you are interested in (e.g. implicit arguments). Is it possible to also display the infoview in term mode proofs?

-- no way to get the infoview to show
example : 1 + 1 = 2 := rfl
-- infoview shows when your cursor is on (or before/after) `by`
example : 1 + 1 = 2 := by rfl

[Utensil Song]

I also wonder this frequently. rfl might not make much difference here, because infoview will show expected type, which happens to be the goal. In more complicated cases, I need infoview to guide me through filling the parameters to the term, e.g.

/-
type mismatch
  Nat.one_add
has type
  ∀ (n : ℕ), 1 + n = Nat.succ n : Prop
but is expected to have type
  1 + 1 = 2 : Prop
-/
example : 1 + 1 = 2 := Nat.one_add

I hope infoview can give me the expected type one parameter by one parameter, guide me through filling the holes, as in tactic mode.

[Utensil Song]

For now, I'm frequently relying on type mismatch to figure out what should I fill, not only in term mode, but also anywhere requires feeding parameters. Sometimes Lean could be really upset by what I fed to it, and gives me really terrifying errors (I can post here if I meet one again), if Lean can realize that I'm just trying to make the term to match a goal/type, and guide me like for proofs, it would be really cool.

[Utensil Song]

Another case that feels like treading on eggs is when giving rewrite rules parameters, it could also use help from infoview.

[Alex Keizer]

If you put a _ in place of your proof, and put your cursor on the _, the info-view will show the info you are looking for

[Utensil Song]

Thanks for the hint, but as frequent as this, can Lean pretend I have a _ after my cursor, so I don't have to insert a _ and move my cursor back to before _. Also don't know if this addresses all use cases @Floris van Doorn has in mind for this question.

[Alex Keizer]

Yes, it would be nice if we can get this info without having to change the term