Maude-help mailing list

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

Dear Maude-Help,

    I have a question about operations. As follows, there are some arithmetic operations and when I load them(ZZ.maude) into maude, I use "red -(1+2)" to test with setting trace on. In my mind, it should be "-1 + -2" and then "-3". However, it is "3" firstly and then "-3" using building-in function. Do we have any other way to define user's function overriding building-in ones.

    Thanks.

========================================================================

fmod ZZ is protecting INT . *** using Maude's built-in integers vars I J K L : Int . *** properties of arithmetic operations eq 0 + I = I . eq I + - I = 0 . eq -(I + J) = - I + - J . eq I - J = I + (- J) . eq 0 * I = 0 . eq - I * J = -(I * J) . eq I * (J + K) = I * J + I * K . eq (I + J) * K = I * K + J * K . cq I * J = (I - 1)* J + J if I > 0 .

endfm

=================================================================

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