input-method: let '\' mark the end of input as ' ' does - Githubissues

leanprover / leanprover.github.io

www

https://lean-lang.org/

15 stars 24 forks source link

input-method: let '\' mark the end of input as ' ' does #11

Closed soonhokong closed 9 years ago