Core Maude Grammar

This chapter describes the syntax of Maude using the following extended BNF notation: the symbols `$\left(\right.$' and `$\left.\right)$' are used as metaparentheses; the symbol `$\mid$' is used to separate alternatives; square bracket pairs, `$[$' and `$]$', enclose optional syntax; `*' indicates zero or more repetitions of preceding unit; `$+$' indicates one or more repetitions of preceding unit; and the string ``x'' denotes x literally. As an application of this notation, A$\left(\right.$, A$\left.\right)$* indicates a non-empty list of A's separated by commas. Finally, %%% indicates comments in the syntactic description, as opposed to comments in the Maude code.