#simp
A user command to run the simplifier.
simp_arg_type.to_pexpr retrieves the pexpr underlying the given simp_arg_type, if there is
one.
simp_arg_type.replace_subexprs calls expr.replace_subexprs on the underlying pexpr, if
there is one, and then prepares the result for use by the simplifier.
The basic usage is #simp e, where e is an expression,
which will print the simplified form of e.
You can specify additional simp lemmas as usual for example using
#simp [f, g] : e, or #simp with attr : e.
(The colon is optional, but helpful for the parser.)
#simp understands local variables, so you can use them to
introduce parameters.