Nonexec

The nonexec attribute allows the user to include statements in a module that are ignored by the Maude rewrite engine. For example we could make the distributive law nonexecutable as follows.

  eq (N + M) * I = (N * I) + (M * I)
    [nonexec metadata "distributive law"] .

Similarly, a rule can be declared with the nonexec attribute in a system module.

Although nonexecutable from the point of view of Core Maude, such statements are part of the semantics of the module and can for example be used at the metalevel for controlled execution or theorem proving purposes.