vscode-lean icon indicating copy to clipboard operation
vscode-lean copied to clipboard

Spacing at end of "Try this" line

Open sgouezel opened this issue 5 years ago • 0 comments

Given

  squeeze_simpa [model_with_corners.left_inv] using hx },

if I click on the suggested output it erases the space between hx and }. This breaks mathlib style convention.

sgouezel avatar Jun 17 '20 19:06 sgouezel