search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
197 stars 35 forks source link

(Support changing abbreviation letter) Support writing math symbols using ; in addition to \ #225

Open JadAbouHawili opened 6 months ago

JadAbouHawili commented 6 months ago

The ; button is easier to reach, and it's allowed in vscode so why not.

joneugster commented 6 months ago

I believe it's only a thing in vscode if you set it in the settings. But I agree, lean4web has the option to choose the abbreviation character. Would be nice to integrate the settings from there.