Skip to content

Remove "\<n" giving "≮"#685

Merged
mhuisi merged 1 commit intoleanprover:masterfrom
kckennylau:patch-2
Dec 17, 2025
Merged

Remove "\<n" giving "≮"#685
mhuisi merged 1 commit intoleanprover:masterfrom
kckennylau:patch-2

Conversation

@kckennylau
Copy link
Contributor

@kckennylau kckennylau commented Oct 27, 2025

because ⟨n is far more common, and instead remapped it to \notlt

Zulip: <n should not produce ≮

@kckennylau kckennylau changed the title Remove "<n" giving "≮" Remove "\<n" giving "≮" Oct 27, 2025
Comment on lines 707 to 708
"<=n": "≰",
"<=>n": "⇎",

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
"<=>n": "",
"n<=": "",
"n<=>": "",

Comment on lines 711 to 712
"<~nn": "≴",
"<~n": "⋦",

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
"<~nn": "",
"<~n": "",
"n<~": "",
"<n~": "",

@mhuisi mhuisi merged commit f15faf1 into leanprover:master Dec 17, 2025
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants