autocompletion problem

Stream: general

[Kevin Buzzard]

I've been writing boilerplate. In this slightly incomplete code

structure ContinuousSMul (M X : Type) : Prop where
structure ContinuousAdd (X : Type) : Prop where

theorem Prod.continuousSMul {M X Y : Type} : ContinuousSMul M (X × Y) := ⟨⟩

theorem Prod.continuousAdd {X Y : Type} : ContinuousAdd (X × Y) := ⟨⟩

example : (ContinuousSMul Nat (Nat × Nat)) ∧ (ContinuousAdd (Nat × Nat)) := by
  exact ⟨Prod.continuousSMul, Prod.continuous⟩ -- put cursor after `s` in `Prod.continuous`
                                               -- and ctrl-space fails for me

I would expect Lean to offer autocomplete suggestions after typing Prod.continuous (an unfinished declaration name) at the end of the code. If I ctrl-space to ask, it offers me neither of the theorems which I've just defined. This surprises me. Is it expected?

[Marc Huisinga]

This looks like a bug to me. Could you file a bug report in the Lean 4 repo?

[Kevin Buzzard]

lean4#5219

[Eric Wieser]

Another fun one:
image.png