[Agda] Type Mismatch in with

[Ashish Mishra]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151106/acd2af61/attachment.html