я даже скипнул фазу рестклиента и сразу юзал его в бабеле

acl2?

Окей, кажется есть

set wildmenu
set wildmode=list:longest,full

Я хотел в консольке подредачить конфиг на серваке,  весь день разбираюсь в этой операционной система, настроил три хоткея.

Выписан из емаксеров

Ну нравится человеку страдать

Ну выписан из рая

Я лишь посмотреть

Да и может в итоге переключусь на какой-нибудь evil хз

Да всё уже, назад нельзя

Печально

Я шучу, если что

Это залипание клавы, да. А залипания мышки там нет.

Да я понял. В имаксе похоже как минимум система получения помощи лучше. В виме я не могу пока понять, как найти ту или иную вещь, не покидая редактор.

книжку почитай

вон сколько понаписывали

Их ещё надо купить

Я смотрел немного на примеры использования ACL2.  Все такие пруверы, которые я видел, по-моему созданы явно не для математиков, а для каких-то других аудиторий, так что даже по туториалам оценить применимость тяжело.  Как я понимаю, он делает полный перебор (м.б. с оптимизациями какими-то).  (1) Это, конечно, полезно как один из инструментов, но в математике это редко работает. (2) Каких-то интересных математику задач там не рассматривается. (3) В примерах не видно итогового текста доказательства — если такого человекочитаемого текста не производится, то это, можно скзаать, вообще не про математику. (4) ACL2 доказывает факты про функции, записанные на языке-подмножестве CL, а про расширяемость я в свое время упоминаний не нашел — звучит не очень обнадеживающе, как будто целевая аудитория и не заинтересована расширять, и ей будет достаточно того, что есть.

Мышь не нужна чтобы решать упражнения, разве что для рисования, и скорее всего без нее будет эффективнее.