CODEWITHSUNDEEP
warningsagda
mmsss
mmsss

Reputation: 273

Yellow highlight in Agda

I write the below code in 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

When I load the above code, I get yellow highlight with 

tt ā‰” tt

at line 8. What is wrong with the code?

Upvotes: 0

Views: 458

Answers (1)

effectfully
effectfully

Reputation: 12715

Perhaps you imported Data.Unit or Data.Unit.Base which introduced another tt (namely the inhabitant of āŠ¤), so Agda is confused about which one to choose. You can write

test_a : š”¹.tt ā‰” tt
test_a = refl

or

import Function

test_a : (š”¹ āˆ‹ tt) ā‰” tt
test_a = refl

Upvotes: 1

Related Questions