From ff33ebe350fd889717bbc7d9678e845a632a0687 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sun, 5 Jan 2025 12:05:58 +0900 Subject: [PATCH] Update README.md --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index c7d0778..156172b 100644 --- a/README.md +++ b/README.md @@ -5,6 +5,7 @@ ## How to type unicode symbols in +- Use a latex_commands-to-unicode_symbols converter like [lucr](https://github.com/shnarazk/lucr) - Use simple-completion extension (But I don't know how to configure it) - Use snippet (CONFIG/snippets/lean4.json) like this (But a newline is inserted after completion):