Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

I don't see any mention of sort Int or operator [[_]] in the attached file.

However the issue is that if two operators declarations are considered to define the same operator if their corresponding domain and range sorts are in the same kind. Two sorts are in the same kind if they are connected directly or indirectly by subsort relations.

So if you want to have two _+_ operators they must be defined on sorts from different kinds. It is also possible to extend the definition of built-in operators such as _+_ however the attributes in the new declaration must be identical to those in the built-in declaration; this can be ensured by giving the single attribute ditto.

Steven

On 3/4/13 1:15 PM, Yiming Li wrote: Dear Helper,

   I have a class in the semantics of programming language using Maude. When I write Maude code, there is a problem that my tutor cannot solve it and therefore ask you.

   

   eq  [[M + N]] = [[M]] + [[N]]

   As above, I want use "+" as two different meanings, one is defined by myself and another is defined by "Int" sort. How can the Maude solve the same symbol? I have tried them, however, the Maude said there was a error that was defined twice. You know (0).Int and (0).Nat can be used to realize the same "0". Do we have the similar way to solve the same operator? 

   I have attached my maude files. Thank you very much.

--
Best regards,
Yiming (Nathan)
-----------------------------------------------------------------------------------------------------
Department of Computer Science
University of Liverpool

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help