Gelbes Highlight in Agda

Question

Ich schreibe den folgenden 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 

Wenn ich den obigen Code laden, erhalte ich gelbe Markierung mit

tt ≡ tt 

in Zeile 8. Was mit dem Code falsch?

Answer 1

Vielleicht importiert Sie Data.Unit oder Data.Unit.Base, die eine andere tt eingeführt (nämlich die Einwohner von ⊤), so ist Agda verwirrt über die man zu wählen. Sie können

test_a : .tt ≡ tt 
test_a = refl 

oder

import Function 

test_a : (∋ tt) ≡ tt 
test_a = refl