The label attribute must be followed by an identifier. Statement labels can be used for tracing and debugging and at the metalevel to name particular axioms. In our numbers example we could label the axiom for idempotency for natural number sets
eq N ; N = N [label natset-idem] .
Syntactic sugar for labels generalizing the Maude 1 style for rule labels is also supported. Then the above label could have also been written
eq [natset-idem] : N ; N = N .