K-user mailing list

[Bram Geron <bgeron AT gmail.com>]

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