intros hover

Stream: lean4

[Filippo A. E. Nuccio]

When hovering on intros the following infoview appears:

intros x ... behaves like intro x ..., but then keeps introducing (anonymous) hypotheses until goal is not of function type

Now, if I try

def bar : Nat → Nat → Nat → Nat := by
  intros

the state is

a✝² a✝¹ a✝ : Nat
⊢ Nat

so lean rightly inserts three anonymous variables. But if I do

def bar : Nat → Nat → Nat → Nat := by
  intros a

the state is

a: Nat
⊢ Nat → Nat → Nat

exactly as with intro a. lean has not inserted the other two anonymous variables. So I think that the infoview is misleading, because the behaviour of intros and intro is different, while those of intro a and intros a are identical.

[Kyle Miller]

@Filippo A. E. Nuccio I made a docstring PR: lean4#2777