1In Maude, types come in two flavors, called sorts and kinds (see Section 3, and the discussion of user-definable data in Section 1.1.2 below).