[Agda] Type Mismatch in with

[Harley Eades III]

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> 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>
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151105/f8ef1dfe/attachment-0001.html