Maude-help mailing list

[Yiming Li <nathan.liyiming AT gmail.com>]

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

Attachment: arithmetic.maude
Description: Binary data