Topic: squeeze_simp eating the end
Yaël Dillies (May 28 2021 at 07:33):
There's a little bug with the
Try thisautomation. Before: image.png
Yaël Dillies (May 28 2021 at 07:34):
end is accidentally brought out of existence.
Kevin Buzzard (May 28 2021 at 07:48):
This might already be in the list of issues. Try poking around here to see if this is already reported.
Shing Tak Lam (May 28 2021 at 08:19):
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 (May 28 2021 at 08:29):
Eric Wieser (May 28 2021 at 08:33):
Ideally we'd do this non-heuristically, and "try this" would specify the position to replace
Last updated: Aug 03 2023 at 10:10 UTC