<div dir="ltr"><div><div>Hi all,</div><div><br></div><div>For some reason, agda cannot infer implicit arguments in the following code. It seems that it should be easy. Why agda cannot do it? Is there a way to fix the problem without explicitly passing the arguments?</div><div><br></div><div>open import Data.List</div><div>open import Relation.Binary.PropositionalEquality</div></div><div><br></div><div>A : Set</div>A = 0 ∷ [] ≡ 0 ∷ []<div><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div>Regards,</div><div dir="ltr">Valery Isaev<br></div></div></div></div></div>
</div></div>