A variable is constrained to range over a particular sort or kind. Variables can be declared on-the-fly in Maude with syntax consisting of an identifier (the variable name), a colon, and another identifier (its sort) or kind expression (its kind). For example, N:Nat declares a variable named N of sort Nat, and X:[Nat] declares a variable named X of kind [Nat].
The scope of an on-the-fly variable declaration is the declaration's occurrence. Thus each such variable must be accompanied by its sort or kind.
A variable can also be declared in a module using the keyword var followed by an identifier (the variable name), followed by a colon with white space before and after, followed by an identifier (its sort) or kind expression (its kind), followed by white space and a period.
var N : Nat . var X : [Nat] .
The scope of such a declaration is the entire module. It has the effect of replacing occurrences of N and X by the on-the-fly versions N:Nat and X:[Nat].
Multiple variables of the same sort can be declared using the keyword vars.
vars M N : Nat . vars X Y : [Nat] .
Both upper and lower case names for variables are possible. However, upper case variable names are more customary in Maude. The syntactic conventions for the acceptable names of variables in variable declarations are the same as those for constant operators, that is, for operators with empty arity. In particular, the underscore `_' cannot be used in the name of a variable, but the colon `:' can; thus the scanning for `:' in order to extract the appropriate sort or kind from an on-the-fly variable declaration is done from right to left.