An expression followed by ; is a command that evaluates the expression and discards the value. Any type is accepted, void included, which allows a call to a void function as a statement.

\dfrac{\Gamma \vdash e : \tau}{\Gamma \vdash e; \dashv \Gamma}\;\textsf{(T-ExprStmt)}

\dfrac{\rho, \sigma \vdash e \Rightarrow v, \sigma'}{\rho, \sigma \vdash e; \Rightarrow \mathsf{normal}, \rho, \sigma'}\;\textsf{(ExprStmt)}

The implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.