K-user mailing list

["Moore, Brandon Michael" <bmmoore AT illinois.edu>]

It's hard to tell what is going on without a minimal example.

One thing I can see is that you defined isInList and isInSubset for the 
generic
type List, which is a different sort than your Record type.

Brandon
________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Abdul Dakkak 
[abduld AT wolfram.com]
Sent: Wednesday, May 08, 2013 12:35 PM
To: k-user
Subject: [K-user] defining subset operator on Lists

I have the following


   syntax Field ::= Id
   syntax RecordItem ::= Field ":" Type
   syntax Record  ::= List{RecordItem,","}


  syntax Bool ::= ListItem "isInList" List [function]
  syntax Bool ::= List "isSubset" List [function]

  rule X:ListItem isInList (_ X _) => true

  rule .List isSubset X:List => true
  rule (L:ListItem Ls:List) isSubset X:List => Ls isSubset X when L isInList 
X ==K true
  rule (L:ListItem Ls:List) isSubset X:List => false when L isInList X =/=K 
true



but when I use it


  rule <k>(S:Record -> T:Type) S':Record => T ...</k>
       when (S isSubset S') ==K true


I get an error stating that it expects S to be of Type ListItem and not 
Record.

-adk-
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user