K-user mailing list

[Bram Geron <bgeron AT gmail.com>]

Thanks!

I didn't know about ==List because it's not in k-prelude.k, but it's 
good to know that it exists.

Cheers, Bram



On Mon 12 Nov 2012 03:21:08 PM CET, Guth, Dwight wrote:
> 1. ==List, =/=List
> 2. List2KLabel LStack(.List{K})
> ------------------------------------------------------------------------
> *From:* 
> k-user-bounces AT cs.uiuc.edu
>  
> [k-user-bounces AT cs.uiuc.edu]
>  on
> behalf of Bram Geron 
> [bgeron AT gmail.com]
> *Sent:* Monday, November 12, 2012 8:18 AM
> *To:* 
> k-user AT cs.uiuc.edu
> *Subject:* [K-user] Equality on lists
>
> Hey guys,
>
> I'm trying to test equality of two Lists, named LStack and RStack. My
> initial thought was to use
>
>     when LStack ==K RStack
>
> at the end of the K rule, but I get a
>
>     [Error] Critical: Variable RStack cannot have sort K at this location. 
> Expected sort List.
>
> My second thought was to use
>
>     when (List2K LStack) ==K (List2K RStack),
>
> then I get a Maude error:
>
>     Error: Warning: <standard input>, line 52 (mod EQUIV): didn't expect 
> token 'List2K_:
>     (repetition of Maude rewrite rule)
>
> This surprises me a lot, because List2K_ has been defined as syntax in
> k-prelude.k.
>
> So I'm wondering about two things. (1) What would be the preferred way
> to compare equality of two lists? (2) Why doesn't List2K work, and
> what would be the preferred way to inject a List into K?
>
> I'm using the nightly build of r8568.
>
> Cheers, Bram
>