infix completion

Stream: lean4

[Julian Berman]

A small thing I noticed in Lean 3 that still seems to be true in Lean 4 is that the Lean server won't suggest completions of infix notation. E.g.:

infix:70  " mul "  => HMul.hMul  -- ditto

#check 2 mu<Tab>

will not suggest mul -- is this something that's any easier now than before (or that anyone else has noticed -- I'm sure lots of infix notation are symbols so maybe it doesn't matter much)?

[Julian Berman]

(Oh, I forgot, this is a dumb question, since completion isn't present at all, so of course it doesn't work for this either. Never mind :)