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

Published 20 hours ago • verified publisher icon leanprover

Triggering an eager replacement with a new abbreviation does not track new abbreviation in LoogleView

Open mhuisi opened this issue 8 months ago • 0 comments

Typing \to\to will yield →\to instead of →→ in the LoogleView.

mhuisi avatar Jun 21 '24 10:06 mhuisi