[Agda] Type Mismatch in with

[Ashish Mishra]

Thanks all for elucidating the concept for me, I got my mistake and got it
working .

Best Regards
Ashish

On Fri, Nov 6, 2015 at 12:37 PM, Harley Eades III <harley.eades at gmail.com>
wrote:

> Andreas, thanks for correcting my mistake. :-)
>
> Very best,
> Harley
>
> On Nov 6, 2015, at 2:20 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>
> Ashish, you need
>
>  a ≟ x   (type a \?= x)
>
> instead of  a ≡ x  or  Dec (a ≡ x).
>
> Cheers, Andreas
>
>
> On 05.11.2015 21:19, Ashish Mishra wrote:
>
> Hi Harley,
> Thanks for the swift reply, Correct me if i am wrong ,
> 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.
>
> P.S. The parameter to *with* 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.
>
> Thanks
>
>
>
>
>
> On Fri, Nov 6, 2015 at 1:02 AM, Harley Eades III <harley.eades at gmail.com
> <mailto:harley.eades at gmail.com <harley.eades at gmail.com>>> wrote:
>
>    Hi, Ashish.
>
>    It looks like the problem is the ‘Dec(_=_ a x)’
>
>    I think this should be 'a = x’ instead.  The former is the type used
>    to show
>    that ‘_=_’ is decidable, and so the type of yes becomes Set.
>
>    Very best,
>    Harley
>
>    On Nov 5, 2015, at 2:18 PM, Ashish Mishra
>    <ashish123.mishragkp at gmail.com
>    <mailto:ashish123.mishragkp at gmail.com <ashish123.mishragkp at gmail.com>>>
> wrote:
>
>    Hi All,
>
>    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.
>
>    /  open import Relation.Nullary.Core/
>    /  lookupelem : { A : Set } ( a : A ) → List' A → Maybe A /
>    /  lookupelem a [] = nothing/
>    /  lookupelem a ( x :: xs ) with Dec( _≡_ a x )/
>    /  lookupelem a ( x :: xs ) | yes _ = just a /
>    /  lookupelem a ( x :: xs ) | no _ = lookupelem a xs /
>
>    The type checker throws an error -
>
>    *Type mismatch*
>    *when checking that the pattern yes _ has type Set*
>
>    where List' is defined same as List from the std-lib , I cant see
>    where the problem is
>
>    Thanks :)
>
>    --
>    Regards,
>    Ashish Mishra
>    Graduate Student,
>    Computer Science and Automation Department,IISc
>    Cell : +91-9611194714
>    Mailto : ashishmishra at csa.iisc.ernet.in
>    <mailto:ashishmishra at csa.iisc.ernet.in <ashishmishra at csa.iisc.ernet.in>
> >
>
>    _______________________________________________
>    Agda mailing list
>    Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se
> <Agda at lists.chalmers.se>>
>    https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
>
> --
> Regards,
> Ashish Mishra
> Graduate Student,
> Computer Science and Automation Department,IISc
> Cell : +91-9611194714
> Mailto : ashishmishra at csa.iisc.ernet.in
> <mailto:ashishmishra at csa.iisc.ernet.in <ashishmishra at csa.iisc.ernet.in>>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>
>
>


-- 
Regards,
Ashish Mishra
Graduate Student,
Computer Science and Automation Department,IISc
Cell : +91-9611194714
Mailto : ashishmishra at csa.iisc.ernet.in
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151106/511c8ab7/attachment-0001.html