问题描述
说我记得一个常数或理论名称，但完全忘记了它的声明位置。也许，我什至不知道在哪个MMT存档中声明它。如何找到源文件？
我可以只打开MMT Shell，加载磁盘上所有的存档，然后发出一些命令find_constant <constant name>吗？这样的命令存在吗？
解决方法
这取决于您对要声明其声明点的事物的了解：
-
如果您一无所知，即说您甚至没有使用该内容的类型检查文件。
然后，找出声明点的最简单方法是使用正则表达式对所有
*.mmt文件进行grep。对于（类型化的）常量，请使用<constant name>\s*?:。它将匹配常量声明，后跟一些可选的空格和冒号。使用Notepad ++，这很容易做到。假设您想知道
congT的声明位置。然后您会这样做：
-
您有一个用于检查所用内容的MMT文件检查类型。
然后使用MMT IntelliJ plugin及其文档树：首先对手边的文件进行类型检查，然后在助手中查找常量的出现：
在这里激活 Navigate 选项特别有用：这样，您可以简单地用鼠标单击要查找其声明点的东西（例如
nat_lit），然后立即拥有它在同伴中显示出来。在此，补充符号显示nat_lit (?NatLiterals)，表示常数是在理论NatLiterals中定义的。理想情况下，您知道该理论的声明位置。从理论上讲，您也可以按住Control键并单击该常量，但是由于我所不知道的原因，目前该行不通。