Ali Kheradmand

The problem somehow got mysteriously fixed by itself after changing some irrelevant parts of the semantics!

Yeah it seems not working. `#sort` is not working either.

Btw, I am using K on commit f1e428f488fe338a9f4994a9da61323d0e86401f

@daejunpark ``` rule (H:HeaderTypeDeclaration _:P4Declarations => .) ... ``` Is not exactly what I wanted, I changed it to ``` rule (H:HeaderTypeDeclaration => .) _:P4Declarations ``` And now it works....

@cos ``` rule (H:HeaderTypeDeclaration => .) _ ``` works @daejunpark It there a place to read about this stuff? I am doing everything **only** by trial and error and have...

@cos are you asking me or Daejun? If it is me, adding ```_``` solved my problem. I don't know if it will be considered as a K's problem or not.

It seems that it is not related to packets being string. I changed the packets structure and still get this kind of errors: An step before error: ``` ( V0...

This is happening in commit 35df078e85e

@daejunpark It seems that the essence of the problem is this; ``` syntax KResult ::= Val | Bool syntax Val ::= "@val" "(" Int "," Int "," Bool ")" syntax...

This one also has the same problem: ``` syntax KResult ::= Val | Bool syntax Val ::= "@val" "(" Int "," Int "," Bool ")" syntax KItem ::= K "%=="...