[Agda] Type Mismatch in with

[Harley Eades III]

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 <mailto: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>
>>>    <mailto:ashish123.mishragkp at gmail.com <mailto: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>
>>>    <mailto:ashishmishra at csa.iisc.ernet.in <mailto:ashishmishra at csa.iisc.ernet.in>>
>>> 
>>>    _______________________________________________
>>>    Agda mailing list
>>>    Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>>
>>>    https://lists.chalmers.se/mailman/listinfo/agda <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>
>> <mailto:ashishmishra at csa.iisc.ernet.in <mailto:ashishmishra at csa.iisc.ernet.in>>
>> 
>> 
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda <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 <mailto:andreas.abel at gu.se>
> http://www2.tcs.ifi.lmu.de/~abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151106/42d7b13c/attachment.html