[Agda] Type Mismatch in with
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Nov 6 08:20:00 CET 2015
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>> 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>> 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 <mailto: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>
>
>
>
> _______________________________________________
> 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/
More information about the Agda
mailing list