[Maude-help] Checking sorts of arguments of polymorphic binary operators

[Lucian Bentea]

 Hi everyone,

 I would have a question related to how Maude parses polymorphic binary 
 operators. Consider the following example:

 sorts S S' Mapping .

 ops a b : -> S [ctor] .
 ops x y : -> S' [ctor] .
 
 op _->_ : Universal Universal -> Mapping [poly (1 2)] .

 I would like to use the binary operator -> to represent the mapping of 
 elements of some arbitrary sort, to elements of another _possibly 
 different_ arbitrary sort.

 The expressions "a -> b" and "x -> y" are both parsed without any 
 errors. However, if I try to reduce "a -> x", I get the error: didn't 
 expect token x: a -> x <---*HERE*

 My question is: does Maude first check that both arguments "a" and "x" 
 are of the same sort before reducing "a -> x"? If this is the case, is 
 there an easy way to define in Maude a polymorphic operator -> which can 
 take arguments of arbitrary, but different sorts?

 Best regards,
 Lucian Bentea