1
$\begingroup$

I am using Lean 4 (4.3) and trying to enter some stylized brackets in Unicode: ⦍ .

Per this question, I tried to hover the mouse in VS Code over its definition:

notation:arg "⦍" a "⦐" => { b | a ∼ b }

But there is no hint for ⦍. However, there is a hint for the next symbol ∼ ("Type ∼ using ~ or \homotopy ...").

Then, I tried to extract something from Emacs, by copying the symbol into a new file a.lean, and typing C-u C-x = over it. But the instructions there (listed below) does not seem to apply to vscode.

             position: 1 of 2 (0%), column: 0
            character: ⦍ (displayed as ⦍) (codepoint 10637, #o24615, #x298d)
              charset: unicode (Unicode (ISO10646))
code point in charset: 0x298D
               script: symbol
               syntax: (⦎   which means: open, matches ⦎
             category: .:Base
             to input: type "C-x 8 RET 298d" or "C-x 8 RET LEFT SQUARE BRACKET WITH TICK IN TOP CORNER"
          buffer code: #xE2 #xA6 #x8D
            file code: #xE2 #xA6 #x8D (encoded by coding system utf-8-unix)
              display: by this font (glyph code):
    ftcrhb:-GNU -FreeSerif-regular-normal-normal-*-15-*-*-*-*-0-iso10646-1 (#x1962)

Character code properties: customize what to show
  name: LEFT SQUARE BRACKET WITH TICK IN TOP CORNER
  general-category: Ps (Punctuation, Open)
  decomposition: (10637) ('⦍')

There is an overlay here:
 From 1 to 2
  face                 show-paren-mismatch
  priority             1000

How can I find the latex style key sequence for ⦍, and in general for symbols when the mouse hover does not show it?

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ 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. $\endgroup$
    – Jason Rute
    Commented Aug 24 at 2:55
  • $\begingroup$ 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. $\endgroup$
    – jthulhu
    Commented Aug 30 at 9:39
  • $\begingroup$ 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. $\endgroup$
    – jthulhu
    Commented Aug 30 at 9:44

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.