Agda中≣运算符的定义位置及模块导入问题咨询

首先明确：Agda标准库（agda-stdlib）中不存在≣（通过\===输入的符号）这个预定义运算符，你执行grep没找到结果是正常的。

可能的原因及解决方向：

• 自定义模块定义：你代码中注释掉了open import Equality，这个被注释的模块大概率就是定义≣的地方。检查项目中是否存在这个本地模块，或者你参考的教程/项目里是否提供了这个模块。
• 符号混淆：Agda标准库中表示命题相等的标准运算符是≡（输入\equiv或\==即可生成），对应的refl也不需要额外参数（你代码里的refl 82是错误写法，正确用法是直接写refl，Agda会自动推导类型）。
• 第三方/旧版本库：如果是参考了某个非标准库或非常旧的标准库版本，需要核对对应库的文档或代码，确认符号的定义位置。

另外补充你代码中的两个小问题：

1. Agda标准库没有Prelude模块，这个模块要么是你本地自定义的，要么是来自第三方库。
2. 标准库中refl是无参数的，正确的相等证明应该写成：

example : (3 ^ 4) ≡ 81
example = refl

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