Скажем, я помню имя константы или теории, но совершенно забыл, где оно объявлено. Возможно, я даже не знаю, в каком ММТ-архиве он заявлен. Как узнать исходный файл?
Могу ли я просто открыть оболочку MMT, загрузить все архивы, которые есть на моем диске, и выполнить какую-нибудь команду find_constant <constant name>? Существует ли такая команда?
Это зависит от того, что вы знаете о предмете, точку объявления которого вы ищете:
Если вы ничего не знаете, т.е. если у вас даже нет файла проверки типов, в котором эта штука используется.
Тогда самый простой способ узнать точку объявления - просто выполнить grep по всем *.mmt файлам с регулярными выражениями. Для (типизированных) констант используйте <constant name>\s*?:. Он будет соответствовать объявлениям констант, за которыми следуют некоторые необязательные пробелы и двоеточие.
С Notepad++ это легко сделать. Скажем, вы хотели знать, где объявлено congT. Тогда вы бы сделали:
У вас есть файл MMT для проверки типов, в котором используется то, что вы ищете.
Затем используйте плагин MMT IntelliJ и его дерево документов: сначала проверьте тип файла под рукой. , а затем поищите в корешке вхождение константы:
Здесь особенно полезна активация параметра Навигация: с его помощью вы можете просто щелкнуть мышью по объекту, точку объявления которого вы ищете (здесь, например, nat_lit), и он сразу же появится в помощнике. Здесь помощник показывает nat_lit (?NatLiterals), что означает, что константа была определена в теории NatLiterals. В идеале вы знаете, где декларируется эта теория.
Теоретически вы также можете нажать на константу, удерживая нажатой клавишу Control, но в настоящее время это не работает по неизвестным мне причинам.
