is mentioned by

Def [[ds]] rho == [[d]] rho for d {d:dec()| d ds }

[decls_mng]

In prior sections: mb declaration mb record mb state machine

Try larger context: GenAutomata