Agda 中的黄色亮点答案

【问题标题】：Yellow highlight in AgdaAgda 中的黄色亮点
【发布时间】：2016-04-26 04:26:40
【问题描述】：

我在 Agda 中编写了以下代码。

open import Relation.Binary.PropositionalEquality
open import Data.Unit

data ???? : Set where
    tt : ????
    ff : ????

test_a : tt ≡ tt
test_a = refl

test_b : ff ≡ ff
test_b = refl

当我加载上面的代码时，我得到黄色高亮

tt ≡ tt

在第 8 行。代码有什么问题？

【问题讨论】：

很抱歉没有包括所有的导入。使用3237465，谢谢指出。仙人掌，感谢您添加所有导入。

标签： warnings agda

【解决方案1】：

也许您导入了Data.Unit 或Data.Unit.Base，其中又引入了另一个tt（即⊤ 的居民），所以Agda 不知道该选择哪一个。你可以写

test_a : ?.tt ≡ tt
test_a = refl

或

import Function

test_a : (? ∋ tt) ≡ tt
test_a = refl

【讨论】：