运算符≣在哪里定义？

Question

我正在尝试编写 Agda 程序，并在模块导入部分中查找包以供参考。

据我所知≣是由

\===

产生的。

Grepping agda-library 和 agda-stdlib 项目没有显示任何内容：

grep -r -E  "===[^=]"  ./agda-stdlib/ ./agda-stdlib/src

module Hell3 where

open import Prelude
open import Reflection
--open import Equality
open import Builtin.Reflection
open import Container.List


example : (3 ^ 4) ≣ 81
example = refl 82

Not in scope:
  ≣ at /home/Hell3.agda:11,19-20
when scope checking ≣

Answer 1

以下片段是正确的。

module Hell3 where
open import Relation.Binary.PropositionalEquality  
open import Data.Nat  
example : 3 ^ 4 ≡ 81
example = refl

感谢 Agda 不和谐频道。 所以我的结论是 HoTTEST 使用标准 API 的自定义定义 - refl 不带参数，应该使用 erefl，正如评论中所述，四元运算符实际上是三元运算符。