<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"><<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">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 <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>> 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 " yes _<br>" 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'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 <<a href="mailto:harley.eades@gmail.com" target="_blank">harley.eades@gmail.com</a><br><<a href="mailto:harley.eades@gmail.com" target="_blank">mailto:harley.eades@gmail.com</a>>> wrote:<br><br> Hi, Ashish.<br><br> It looks like the problem is the ‘Dec(_=_ a x)’<br><br> I think this should be '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> <<a href="mailto:ashish123.mishragkp@gmail.com" target="_blank">ashish123.mishragkp@gmail.com</a><br> <<a href="mailto:ashish123.mishragkp@gmail.com" target="_blank">mailto:ashish123.mishragkp@gmail.com</a>>> 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' 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' 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> <<a href="mailto:ashishmishra@csa.iisc.ernet.in" target="_blank">mailto:ashishmishra@csa.iisc.ernet.in</a>><br><br> _______________________________________________<br> Agda mailing list<br> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><span> </span><<a href="mailto:Agda@lists.chalmers.se" target="_blank">mailto: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></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><<a href="mailto:ashishmishra@csa.iisc.ernet.in" target="_blank">mailto:ashishmishra@csa.iisc.ernet.in</a>><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 <>< 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>