<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="">Andreas, thanks for correcting my mistake. :-)<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 6, 2015, at 2:20 AM, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de" class="">andreas.abel@ifi.lmu.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class=""> 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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Hi Harley,<br class="">Thanks for the swift reply, Correct me if i am wrong ,<br class="">The issue here is that the typechecker did not find the type of " yes _<br class="">" as Set which it is looking for , although i am not sure why , because<br class="">the type of yes _ is indeed a Set as per the definition of Dec which is<br class="">of type Set.<br class=""><br class="">P.S. The parameter to *with* needs to be a proposition if I am correct<br class=""> so I don't see Dec ( = a x ) as the issue , moreover replacing it by<br class="">(a = x ) still gives the same error.<br class=""><br class="">Thanks<br class=""><br class=""><br class=""><br class=""><br class=""><br class="">On Fri, Nov 6, 2015 at 1:02 AM, Harley Eades III <<a href="mailto:harley.eades@gmail.com" class="">harley.eades@gmail.com</a><br class=""><<a href="mailto:harley.eades@gmail.com" class="">mailto:harley.eades@gmail.com</a>>> wrote:<br class=""><br class=""> Hi, Ashish.<br class=""><br class=""> It looks like the problem is the ‘Dec(_=_ a x)’<br class=""><br class=""> I think this should be 'a = x’ instead. The former is the type used<br class=""> to show<br class=""> that ‘_=_’ is decidable, and so the type of yes becomes Set.<br class=""><br class=""> Very best,<br class=""> Harley<br class=""><br class=""><blockquote type="cite" class=""> On Nov 5, 2015, at 2:18 PM, Ashish Mishra<br class=""> <<a href="mailto:ashish123.mishragkp@gmail.com" class="">ashish123.mishragkp@gmail.com</a><br class=""> <<a href="mailto:ashish123.mishragkp@gmail.com" class="">mailto:ashish123.mishragkp@gmail.com</a>>> wrote:<br class=""><br class=""> Hi All,<br class=""><br class=""> I am new to agda programming, please help me understanding what is<br class=""> wrong here in the function to get an element from the list if present.<br class=""><br class=""> / open import Relation.Nullary.Core/<br class=""> / lookupelem : { A : Set } ( a : A ) → List' A → Maybe A /<br class=""> / lookupelem a [] = nothing/<br class=""> / lookupelem a ( x :: xs ) with Dec( _≡_ a x )/<br class=""> / lookupelem a ( x :: xs ) | yes _ = just a /<br class=""> / lookupelem a ( x :: xs ) | no _ = lookupelem a xs /<br class=""><br class=""> The type checker throws an error -<br class=""><br class=""> *Type mismatch*<br class=""> *when checking that the pattern yes _ has type Set*<br class=""><br class=""> where List' is defined same as List from the std-lib , I cant see<br class=""> where the problem is<br class=""><br class=""> Thanks :)<br class=""><br class=""> --<br class=""> 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 :<span class="Apple-converted-space"> </span><a href="mailto:ashishmishra@csa.iisc.ernet.in" class="">ashishmishra@csa.iisc.ernet.in</a><br class=""> <<a href="mailto:ashishmishra@csa.iisc.ernet.in" class="">mailto:ashishmishra@csa.iisc.ernet.in</a>><br class=""><br class=""> _______________________________________________<br class=""> Agda mailing list<br class=""> <a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><span class="Apple-converted-space"> </span><<a href="mailto:Agda@lists.chalmers.se" class="">mailto:Agda@lists.chalmers.se</a>><br class=""> <a href="https://lists.chalmers.se/mailman/listinfo/agda" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class=""></blockquote><br class=""><br class=""><br class=""><br class="">--<br class="">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 :<span class="Apple-converted-space"> </span><a href="mailto:ashishmishra@csa.iisc.ernet.in" class="">ashishmishra@csa.iisc.ernet.in</a><br class=""><<a href="mailto:ashishmishra@csa.iisc.ernet.in" class="">mailto:ashishmishra@csa.iisc.ernet.in</a>><br class=""><br class=""><br class=""><br class="">_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class=""><a href="https://lists.chalmers.se/mailman/listinfo/agda" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class=""><br class=""></blockquote><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">--<span class="Apple-converted-space"> </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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><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; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">http://www2.tcs.ifi.lmu.de/~abel/</a></div></blockquote></div><br class=""></div></body></html>