mathlib documentation

tactic.simp_command

#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.

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.