squeeze_simp eating the end

Stream: general

[Yaël Dillies]

There's a little bug with the Try thisautomation. Before: image.png

[Yaël Dillies]

After: image.png
The end is accidentally brought out of existence.

[Kevin Buzzard]

This might already be in the list of issues. Try poking around here to see if this is already reported.

[Shing Tak Lam]

This is probably an issue with vscode-lean and not with mathlib/squeeze_simp specifically. If I had to guess it's probably https://github.com/leanprover/vscode-lean/blob/master/src/tacticsuggestions.ts#L79-L109 . Since currently it replaces until newline/punctuation/..., but it doesn't seem to look for end at the end of the line.

[Shing Tak Lam]

leanprover/vscode-lean#271

[Eric Wieser]

Ideally we'd do this non-heuristically, and "try this" would specify the position to replace