<div dir="ltr"><div>Hi Harley,</div>Thanks for the swift reply, Correct me if i am wrong , <div>The issue here is that the typechecker did not find the type of " yes _ " as Set which it is looking for , although i am not sure why , because the type of yes _ is indeed a Set as per the definition of Dec which is of type Set.</div><div><br></div><div>P.S. The parameter to <b>with</b> needs to be a proposition if I am correct so I don't see Dec ( = a x ) as the issue , moreover replacing it by (a = x ) still gives the same error. </div><div><br></div><div>Thanks </div><div><br></div><div><br><div><br></div><div><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Nov 6, 2015 at 1:02 AM, Harley Eades III <span dir="ltr"><<a href="mailto:harley.eades@gmail.com" target="_blank">harley.eades@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Hi, Ashish.<div><br></div><div>It looks like the problem is the ‘Dec(_=_ a x)’</div><div><br></div><div>I think this should be 'a = x’ instead. The former is the type used to show</div><div>that ‘_=_’ is decidable, and so the type of yes becomes Set.</div><div><br></div><div>Very best,</div><div>Harley</div><div><br><div><blockquote type="cite"><div><div class="h5"><div>On Nov 5, 2015, at 2:18 PM, Ashish Mishra <<a href="mailto:ashish123.mishragkp@gmail.com" target="_blank">ashish123.mishragkp@gmail.com</a>> wrote:</div><br></div></div><div><div><div class="h5"><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' 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' 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>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></div></div>
_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br></div></blockquote></div><br></div></div></blockquote></div><br><br clear="all"><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>