vscode-Infoview: goals accomplished but not

Stream: lean4

[Nick Chopper]

def ff (f: Nat → Nat) : Nat := by exact f f

there is an application type mismatch but tactic state says goals accomplished

[Brandon Brown]

Yeah I guess the Lean4 extension isn't as polished as Lean3, so don't necessarily trust it if it says goals accomplished, make sure there aren't any other errors.

[Mac]

I would note that, in a manner of speaking, the goal was accomplished, f f does technically have type Nat, thus it completes the goal. The problem is simply that f f is invalid, hence the other error. So this might be considered the expected behavior

[Brandon Brown]

But it's not even just related to being type correct. e.g. put this in a blank Lean4 file:

example : ∀ (n m : Nat), (n + m) = (m + n) := by
  intros n m
  apply

for me it says "goals accomplished" even though it's an invalid thing and it shows a squiggly red line "unexpected end of input" as it should.