<div dir="ltr"><div><div>Can someone tell me if the code fragment below is supposed to work? It gives me yellow, but it works fine when I replace `it` by the (unique) solution `is-zero`.<br><br><div style="margin-left:40px">it : {A : Set} {{_ : A}} → A<br>it {{x}} = x<br><br>data IsZero : Nat → Set where<br>  instance<br>    is-zero : IsZero 0<br><br>test : IsZero _<br>test = it<br></div></div><br>Cheers,<br></div>Jesper<br></div>