Zulip Chat Archive

Stream: lean4

Topic: Typing the Placeholder char


Steven Ulin (Sep 28 2021 at 21:26):

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 (Sep 28 2021 at 21:27):

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

Steven Ulin (Sep 28 2021 at 21:29):

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 (Sep 28 2021 at 21:33):

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

Alex J. Best (Sep 28 2021 at 21:33):

I think its \.

Leonardo de Moura (Sep 28 2021 at 21:37):

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

Steven Ulin (Sep 28 2021 at 21:39):

Thanks \. works so does the period :)

Steven Ulin (Sep 28 2021 at 21:40):

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 (Sep 28 2021 at 21:41):

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

Steven Ulin (Sep 28 2021 at 21:50):

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

Steven Ulin (Sep 28 2021 at 21:50):

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

Steven Ulin (Sep 28 2021 at 22:27):

Nvm on the pull request


Last updated: Dec 20 2023 at 11:08 UTC