<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Hi, Ashish.<div class=""><br class=""></div><div class="">It looks like the problem is the ‘Dec(_=_ a x)’</div><div class=""><br class=""></div><div class="">I think this should be 'a = x’ instead. The former is the type used to show</div><div class="">that ‘_=_’ is decidable, and so the type of yes becomes Set.</div><div class=""><br class=""></div><div class="">Very best,</div><div class="">Harley</div><div class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Nov 5, 2015, at 2:18 PM, Ashish Mishra <<a href="mailto:ashish123.mishragkp@gmail.com" class="">ashish123.mishragkp@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hi All,<div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class=""><div class=""> </div><div class=""><i class=""> open import Relation.Nullary.Core</i></div><div class=""><i class=""> lookupelem : { A : Set } ( a : A ) → List' A → Maybe A </i></div><div class=""><i class=""> lookupelem a [] = nothing</i></div><div class=""><i class=""> lookupelem a ( x :: xs ) with Dec( _≡_ a x )</i></div><div class=""><i class=""> lookupelem a ( x :: xs ) | yes _ = just a </i></div><div class=""><i class=""> lookupelem a ( x :: xs ) | no _ = lookupelem a xs </i></div><div class=""><br class=""></div><div class="">The type checker throws an error -</div><div class=""><br class=""></div><div class=""><div class=""><b class="">Type mismatch</b></div><div class=""><b class="">when checking that the pattern yes _ has type Set</b></div></div><div class=""><br class=""></div><div class="">where List' is defined same as List from the std-lib , I cant see where the problem is </div><div class=""><br class=""></div><div class="">Thanks :)</div><div class=""><br class=""></div>-- <br class=""><div class="gmail_signature">Regards,<br class="">Ashish Mishra<br class="">Graduate Student,<br class="">Computer Science and Automation Department,IISc<br class="">Cell : +91-9611194714<br class="">Mailto : <a href="mailto:ashishmishra@csa.iisc.ernet.in" target="_blank" class="">ashishmishra@csa.iisc.ernet.in</a><br class=""><br class=""></div>
</div></div>
_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></div></body></html>