search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
169 stars 48 forks source link

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

Open mhuisi opened 5 months ago

mhuisi commented 5 months ago

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