Как мне набрать m≤n в режиме Agda Emacs, чтобы он не превратился в m≰? - PullRequest
3 голосов
/ 22 мая 2019

Как лучше всего набрать что-то вроде m≤n в режиме Agma Emacs?

Если я наберу m \ <</kbd> = n Я получу m≰, что раздражает .

Мой текущий обходной путь - набрать m \ <</kbd> = Пробел Забой n но это не очень эргономично.

Есть ли что-то, что я могу сделать, не требуя, чтобы я набрал бесполезный ключ, а затем немедленно удалил его с помощью backspace?

Ответы [ 2 ]

2 голосов
/ 28 мая 2019

Другой вариант - использовать Ctrl + g , чтобы выйти из режима «композиции персонажей».

Таким образом, чтобы ввести m≤n, вы можете набрать м \ <</kbd> = ( Ctrl + g ) n

2 голосов
/ 22 мая 2019

Если вы нажмете C-u C-c =, когда курсор находится на символе, вы получите информацию об этом. Строка input описывает различные способы ввода.

Похоже, \leqslant не страдает от дополнительного n превращения в . Однако, это более короткий, чтобы напечатать пробел и затем стереть это.

...