Timeline for How to enter in Lean 4 the unicode for "LEFT SQUARE BRACKET WITH TICK IN TOP CORNER"
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 30 at 9:44 | comment | added | jthulhu |
To be more specific, if you use C-u C-x =, Emacs will show how to input a character regardless of the mechanism used. In your case, it can't be input with Lean's input method, but it can using Emacs' native code point insertion mechanism. But if it were possible to input it using Lean's input method, it would tell you something like type "\_o" with Lean input method. C-c C-k only shows what is possible inputting with Lean's input method, which is similar to the one present in VS Code.
|
|
| Aug 30 at 9:39 | comment | added | jthulhu |
The instructions you see in Emacs to input that characters are not related to Lean. Rather, Emacs allows you to input any unicode character if you know its code point, and that's what you asked it. If you want instead to ask it how to input a character using Lean's plugin support (which I assume to have similar capacities in VS Code and in Emacs), you have to use the C-c C-k shortcut while having the point on the character. If you try this with the character you've asked for, it simply answers ⦍ can’t be input by the current input method, which is to say, there is no shortcut bound for it.
|
|
| Aug 24 at 2:55 | comment | added | Jason Rute | I think that these unicode shortcuts come from this file in the vs code Lean plugin and that the emacs Lean plugin copies from that file. If I'm right about that, I guess you would have to ask to have your symbol added or find another workaround to type it. | |
| Aug 23 at 22:23 | history | asked | tinlyx | CC BY-SA 4.0 |