Блог

Допустим, я помню имя константы или теории, но совершенно забыл, где оно объявлено. Возможно, я даже не знаю, в каком архиве MMT она объявлена. Как я могу узнать исходный файл?

Могу ли я просто открыть оболочку MMT, загрузить все архивы, которые у меня есть на диске, и выполнить какую-либо команду find_constant <constant name> ? Существует ли такая команда?

Это зависит от того, что вы знаете о вещи, точку объявления которой вы ищете:

• Если вы ничего не знаете, т.Е. Если у вас даже нет файла проверки типов, в котором используется эта вещь.

  Тогда самый простой способ выяснить точку объявления — просто выполнить grep по всем *.mmt файлам с регулярными выражениями. Для (типизированных) констант используйте <constant name>s*?: . Он будет соответствовать объявлениям констант, за которыми следуют некоторые необязательные пробелы и двоеточие.

  С Notepad это легко сделать. Допустим, вы хотели знать, где congT объявлено. Тогда вы бы сделали:

  

• У вас есть файл MMT для проверки типов, в котором используется то, что вы ищете.

  Затем используйте плагин MMT IntelliJ и его дерево документов: сначала введите нужный файл, а затем посмотрите в sidekick на наличие константы:

  

  Здесь особенно полезна активация опции навигации: с ее помощью вы можете просто щелкнуть мышью по объекту, точку объявления которого вы ищете (например, здесь nat_lit ), и он сразу же отобразится в sidekick . Здесь sidekick показывает nat_lit (?NatLiterals) , что константа была определена в теории NatLiterals . В идеале вы знаете, где объявлена эта теория.

  Теоретически вы также можете щелкнуть по константе, но в настоящее время это не работает по причинам, не зависящим от моего понимания.