Maude-help mailing list

[zhangmin <zhmtechie AT gmail.com>]

Hi, all:

I have  a functional module which cannot be parsed by Full Maude, but
can be admitted by Core Maude.  The problem is probably caused by the
symbol "=". Here is a toy example:

(fmod EQ is 
    sort A .
    op _=_ : A A -> Bool [comm] .
    op s_ : A -> A .

    vars A1 A2 : A .
    eq (s A1 = s A2) = (A1 = A2) .
endfm)

I have the following feedback from Full Maude after feeding the above
module into Full Maude. 

Warning: Ambiguous parsing for ((s A1 = s A2))=((A1 = A2))
Error: no parse for eq(s A1 = s A2) ~ (A1 = A2)


If I choose other symbol like "~" instead of "=" to define the equation
relation on A, the module can be successfully parsed by Full Maude. 

Are there some other better alternatives to avoid this issue, because we
may not want to ask users not to choose the symbol "=" to define their
own equation relations?

Best regards, 
Zhang Min