vscode-lean4
vscode-lean4 copied to clipboard
"subexpression had been modified" not shown direcly after `rw`
In line 2, col 8 here, the green highlighting doesn't show, I need to add an additional space.
example (p : x = y) (q : y = z) : x = z := by
rw [p]