Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove '' and add ⟨⟩ autopairs in Lean #10680

Closed
ashl3y-v opened this issue May 4, 2024 · 3 comments
Closed

Remove '' and add ⟨⟩ autopairs in Lean #10680

ashl3y-v opened this issue May 4, 2024 · 3 comments
Labels
C-enhancement Category: Improvements

Comments

@ashl3y-v
Copy link
Contributor

ashl3y-v commented May 4, 2024

Add an auto-pairs section to the lean configuration with ⟨⟩ and without ''
Rationale: ⟨⟩ is very commonly used for pattern matching and essentially always used in a pair, and ' is also very commonly used for denoting "prime" almost never used in a pair. If only using one ' the pairing isn't an issue, but when trying to type two, the pairing creates ''' instead, and the same issue is present when trying to type four, etc.

[[language]]
name = "lean"
...

[language.auto-pairs]
'(' = ')'
'{' = '}'
'[' = ']'
'"' = '"'
'`' = '`'
'⟨' = '⟩'
@ashl3y-v ashl3y-v added the C-enhancement Category: Improvements label May 4, 2024
@ashl3y-v
Copy link
Contributor Author

ashl3y-v commented May 4, 2024

Also I should mention that I've tested this and there seem to be no problems with using a 3 byte character for pairs, also see #3964 and #3946.

@pascalkuthe
Copy link
Member

a small config change like this doesn't need an issue, please open a PR if you want to see this changed

@ashl3y-v
Copy link
Contributor Author

ashl3y-v commented May 5, 2024

Okay sorry I'm not too familiar with contributing I'll do that

@ashl3y-v ashl3y-v closed this as completed May 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
C-enhancement Category: Improvements
Projects
None yet
Development

No branches or pull requests

2 participants