<div dir="ltr">Hi All,<div><br></div><div>I am new to agda programming, please help me understanding what is wrong here in the function to get an element from the list if present.</div><div><br></div><div><div>    </div><div><i>  open import Relation.Nullary.Core</i></div><div><i>  lookupelem : { A : Set } ( a : A ) → List&#39; A → Maybe A </i></div><div><i>  lookupelem a [] = nothing</i></div><div><i>  lookupelem a ( x :: xs ) with Dec( _≡_ a x )</i></div><div><i>  lookupelem a ( x :: xs ) | yes _ = just a </i></div><div><i>  lookupelem a ( x :: xs ) | no _ = lookupelem a xs </i></div><div><br></div><div>The type checker throws an error -</div><div><br></div><div><div><b>Type mismatch</b></div><div><b>when checking that the pattern yes _ has type Set</b></div></div><div><br></div><div>where List&#39; is defined same as List from the std-lib , I cant see where the problem is </div><div><br></div><div>Thanks :)</div><div><br></div>-- <br><div class="gmail_signature">Regards,<br>Ashish Mishra<br>Graduate Student,<br>Computer Science and Automation Department,IISc<br>Cell : +91-9611194714<br>Mailto : <a href="mailto:ashishmishra@csa.iisc.ernet.in" target="_blank">ashishmishra@csa.iisc.ernet.in</a><br><br></div>
</div></div>