Special

Many operators in predefined modules (see Chapters 7 and 11) have the special attribute in their declarations. This means that they are to be treated as built-in operators, so that, instead of having the standard treatment of any user-defined operator, they are associated with appropriate C++ code by ``hooks'' which are specified following the special attribute identifier.

For example, the file prelude.maude contains a predefined module NAT for natural numbers and usual operations on them (see Section 7.2). Among others, the declarations in the NAT module for the operations of addition and of quotient of integer division, and for a less than predicate are the following:

    op _+_ : NzNat Nat -> NzNat
          [assoc comm prec 33
           special (id-hook ACU_NumberOpSymbol (+)
                    op-hook succSymbol (s_ : Nat ~> NzNat))] .
    op _+_ : Nat Nat -> Nat [ditto] .

    op _quo_ : Nat NzNat -> Nat
          [prec 31 gather (E e)
           special (id-hook NumberOpSymbol (quo)
                    op-hook succSymbol (s_ : Nat ~> NzNat))] .

    op _<_ : Nat Nat -> Bool
          [prec 37
           special (id-hook NumberOpSymbol (<)
                    op-hook succSymbol (s_ : Nat ~> NzNat)
                    term-hook trueTerm (true)
                    term-hook falseTerm (false))] .

Notice that the special attribute exists in order to bind Maude syntax to built-in C++ functionality. It is absolutely not for users to mess with and it is absolutely not backwards compatible; this is why Maude will sometimes crash or become unstable if the prelude from a different version is loaded. For the same reason, other operator attributes that appear together with special in an operator declaration cannot be modified either.