<div dir="ltr">Thanks all for elucidating the concept for me, I got my mistake and got it working .<div><br></div><div>Best Regards </div><div>Ashish</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Nov 6, 2015 at 12:37 PM, Harley Eades III <span dir="ltr">&lt;<a href="mailto:harley.eades@gmail.com" target="_blank">harley.eades@gmail.com</a>&gt;</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">Andreas, thanks for correcting my mistake. :-)<div><br></div><div>Very best,</div><div>Harley</div><div><div class="h5"><div><br><div><blockquote type="cite"><div>On Nov 6, 2015, at 2:20 AM, Andreas Abel &lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt; wrote:</div><br><div><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">Ashish, you need</span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important"> a ≟ x   (type a \?= x)</span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">instead of  a ≡ x  or  Dec (a ≡ x).</span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">Cheers, Andreas</span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">On 05.11.2015 21:19, Ashish Mishra wrote:</span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><blockquote type="cite" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px">Hi Harley,<br>Thanks for the swift reply, Correct me if i am wrong ,<br>The issue here is that the typechecker did not find the type of &quot; yes _<br>&quot; as Set which it is looking for , although i am not sure why , because<br>the type of yes _ is indeed a Set as per the definition of Dec which is<br>of type Set.<br><br>P.S. The parameter to *with* needs to be a proposition if I am correct<br> so I don&#39;t see Dec ( = a x )  as the issue , moreover replacing it by<br>(a = x  ) still gives the same error.<br><br>Thanks<br><br><br><br><br><br>On Fri, Nov 6, 2015 at 1:02 AM, Harley Eades III &lt;<a href="mailto:harley.eades@gmail.com" target="_blank">harley.eades@gmail.com</a><br>&lt;<a href="mailto:harley.eades@gmail.com" target="_blank">mailto:harley.eades@gmail.com</a>&gt;&gt; wrote:<br><br>   Hi, Ashish.<br><br>   It looks like the problem is the ‘Dec(_=_ a x)’<br><br>   I think this should be &#39;a = x’ instead.  The former is the type used<br>   to show<br>   that ‘_=_’ is decidable, and so the type of yes becomes Set.<br><br>   Very best,<br>   Harley<br><br><blockquote type="cite">   On Nov 5, 2015, at 2:18 PM, Ashish Mishra<br>   &lt;<a href="mailto:ashish123.mishragkp@gmail.com" target="_blank">ashish123.mishragkp@gmail.com</a><br>   &lt;<a href="mailto:ashish123.mishragkp@gmail.com" target="_blank">mailto:ashish123.mishragkp@gmail.com</a>&gt;&gt; wrote:<br><br>   Hi All,<br><br>   I am new to agda programming, please help me understanding what is<br>   wrong here in the function to get an element from the list if present.<br><br>   /  open import Relation.Nullary.Core/<br>   /  lookupelem : { A : Set } ( a : A ) → List&#39; A → Maybe A /<br>   /  lookupelem a [] = nothing/<br>   /  lookupelem a ( x :: xs ) with Dec( _≡_ a x )/<br>   /  lookupelem a ( x :: xs ) | yes _ = just a /<br>   /  lookupelem a ( x :: xs ) | no _ = lookupelem a xs /<br><br>   The type checker throws an error -<br><br>   *Type mismatch*<br>   *when checking that the pattern yes _ has type Set*<br><br>   where List&#39; is defined same as List from the std-lib , I cant see<br>   where the problem is<br><br>   Thanks :)<br><br>   --<br>   Regards,<br>   Ashish Mishra<br>   Graduate Student,<br>   Computer Science and Automation Department,IISc<br>   Cell : +91-9611194714<br>   Mailto :<span> </span><a href="mailto:ashishmishra@csa.iisc.ernet.in" target="_blank">ashishmishra@csa.iisc.ernet.in</a><br>   &lt;<a href="mailto:ashishmishra@csa.iisc.ernet.in" target="_blank">mailto:ashishmishra@csa.iisc.ernet.in</a>&gt;<br><br>   _______________________________________________<br>   Agda mailing list<br>   <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><span> </span>&lt;<a href="mailto:Agda@lists.chalmers.se" target="_blank">mailto:Agda@lists.chalmers.se</a>&gt;<br>   <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br></blockquote><br><br><br><br>--<br>Regards,<br>Ashish Mishra<br>Graduate Student,<br>Computer Science and Automation Department,IISc<br>Cell : +91-9611194714<br>Mailto :<span> </span><a href="mailto:ashishmishra@csa.iisc.ernet.in" target="_blank">ashishmishra@csa.iisc.ernet.in</a><br>&lt;<a href="mailto:ashishmishra@csa.iisc.ernet.in" target="_blank">mailto:ashishmishra@csa.iisc.ernet.in</a>&gt;<br><br><br><br>_______________________________________________<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><br></blockquote><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">--<span> </span></span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.</span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">Department of Computer Science and Engineering</span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">Chalmers and Gothenburg University, Sweden</span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><a href="mailto:andreas.abel@gu.se" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px" target="_blank">andreas.abel@gu.se</a><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><a href="http://www2.tcs.ifi.lmu.de/~abel/" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a></div></blockquote></div><br></div></div></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>