[Agda] Type Mismatch in with

[Ashish Mishra]

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