Agda中的黃色突出顯示

我在Agda中編寫了下面的代碼。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.什麼是錯的代碼？

來源

2016-04-26 mmsss

對不起，不包括所有的進口。要使用3237465，謝謝你指出。仙人掌，感謝您添加所有的進口。 – mmsss

也許你輸入了Data.Unit或Data.Unit.Base，它引入了另一個tt（即⊤的居民），所以Agda對選擇哪一個感到困惑。你可以寫

test_a : .tt ≡ tt 
test_a = refl

或

import Function 

test_a : (∋ tt) ≡ tt 
test_a = refl

來源

2016-04-26 04:55:28 user3237465

Agda中的黃色突出顯示

回答

相關問題