Inconsistency vscode infoview with `induction ... with cas`

Stream: lean4

[Alex Keizer]

I ran into some confusing behaviour when writing induction y with case mk a b =>.
Now I figure that it should be induction y with | mk a b =>, but the error is shown very far from the place where the actual problem occurred.
Furthermore, the vscode infoview keeps working and updating the tactic state, so it seems to think with case is fine.

For example,

example (y : Nat × Nat) : True :=
by
  induction y with case mk a b =>
    -- The infoview keeps working
    have other : a = a := by rfl
    -- `other` is shown in the infoview as expected
    constructor
    -- infoview shows: goals accomplished!


-- But here it finally errors with `expected |`
def foo := "Foo"



example (y : Nat × Nat) : True :=
by
  induction y with case mk a b =>
    -- no error shows up here, but the infoview does stop updating
    apply nonexistent;
    constructor

-- The first error appears here, `expected |`
def bar := "BAR"

This is especially confusing in larger proofs, where the error may occur off-screen

[Sebastian Ullrich]

with can be followed by a tactic that is evaluated for every branch, so this is by design

[Sebastian Ullrich]

Though perhaps a different choice of syntax could make that clearer

[Alex Keizer]

Hmm, then maybe the | should be optional, since that tactic might close all goals. That fixes the first example.
Then, if the | is omitted, maybe we can also stop suppressing errors in the tactic, so the second example will error at apply nonexistent