Typing the Placeholder char

Stream: lean4

[Steven Ulin]

Hey yall I'm trying to type the placeholder char · for simple lambdas like ( · + 1). Does anyone know how to enter · in vscode? \cdot doesn't seem to work

[Henrik Böving]

In emacs lean4-mode its just \dot...I'd guess both of them have the same bindings?

[Steven Ulin]

Hrmm I'm using the vim extension in vscode. \dot and \cdot produce a unicode dot, but the code errors unless I copy the dot from the leanprover github

[Steven Ulin]

It looks like my vscode extension is producing "⬝ miscellaneous symbols and arrows u+02b1d" instead of "· middle dot"

[Alex J. Best]

I think its \.

[Leonardo de Moura]

@Steven Ulin We also have support for the ASCII version (. + 1)

[Steven Ulin]

Thanks \. works so does the period :)

[Steven Ulin]

I found what is going on in the code:
https://github.com/leanprover/vscode-lean4/blob/3888d94cae045e93944645d4ac085970b57279c7/vscode-lean4/src/abbreviation/abbreviations.json

[Steven Ulin]

There are some Black Very Small Squares “⬝” (U+2B1D) in this file instead of Middle Dots “·” (U+00B7)

[Steven Ulin]

Well I made a pull request so other people don't wonder why their code isn't working

[Steven Ulin]

https://github.com/leanprover/vscode-lean4/pull/39

[Steven Ulin]

Nvm on the pull request