-
-
Notifications
You must be signed in to change notification settings - Fork 3.1k
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
Ligatures /\ and \/ for Coq #738
Comments
(Also, I'm not sure if you're aware, but CoqIDE seem to display ligatures just fine without any additional configurations). |
I used to have those but they indeed conflicted with regexps in particular. We could require whitespaces around, that should solve most of the issues I believe. Would that work? What other characters might surroud those? E.g. brackets, parens, newline etc? |
Yes absolutely ! |
I'm using Coq on a daily basis.
Ligatures (such as =>, ->, <->, =?, :=, !=, etc.) are really helping, they make a huge difference in proof readability.
I wish there were ligatures for 'logical and' symbol (u+2227, written /\ in Coq) and 'logical or' symbol (u+2228, written \/ in Coq). Is that something you've considered to add ?
Nevertheless, I can see cases where you would want to write /\ or \/ without triggering the ligatures though, so they could be deactivated by default, so one would have to rebuild the font to use them? Or could it be done through specific rules such as requiring spaces around the symbols ?
Once again, thank you.
The text was updated successfully, but these errors were encountered: