Intellij IDEA Arend插件缺失标准库Order.Lattice下meet-monotone函数

问题根因 #

你遇到的报错核心原因是IntelliJ Arend插件默认绑定的标准库版本，和你手动从官网下载的标准库版本不匹配：meet-monotone是较高版本标准库新增的API，你当前项目配置的langVersion: 1.6.0.1对应的插件内置标准库未收录该函数。

解决方案 #

方案1：替换IDE绑定的标准库 #

直接将插件默认的旧标准库替换为你手动下载的完整版本：

• 打开IntelliJ IDEA设置，依次进入语言和框架 -> Arend配置页
• 找到标准库路径选项，手动选择你下载解压后的官网标准库根目录
• 保存配置后重启IDE，重新加载项目即可识别meet-monotone函数

方案2：匹配版本号 #

如果替换库后仍然报错，需要检查你下载的标准库要求的最低Arend语言版本：

• 如果版本要求高于1.6.0.1，先升级Arend IDE插件到对应版本
• 将项目根目录下arend.yaml中的langVersion字段修改为和标准库匹配的版本号，重新构建项目即可

方案3：临时本地实现 #

如果暂时不想调整版本配置，可以直接在你的项目中补充meet-monotone的实现，代码如下：

\func meet-monotone {A : \Type} {M : MeetSemilattice A} {a1 a2 b1 b2 : A} (a<= : a1 <= a2) (b<= : b1 <= b2) : a1 /\ b1 <= a2 /\ b2
  => <=-trans (meet-universal (<=-trans meet-left a<=) (<=-trans meet-right b<=))

内容的提问来源于stack exchange，提问作者warmte