tactic.simp_command - mathlib3 docs

#simp #

A user command to run the simplifier.

source

meta def tactic.simp_arg_type.to_pexpr :

tactic.simp_arg_type → option pexpr

simp_arg_type.to_pexpr retrieves the pexpr underlying the given simp_arg_type, if there is one.

source

meta def tactic.simp_arg_type.replace_subexprs :

tactic.simp_arg_type → list (expr × expr) → tactic.simp_arg_type

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.

source

meta def tactic.simp_cmd (_x : interactive.parse (lean.parser.tk "#simp")) :

lean.parser unit

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.

source

def tactic_doc.command.#simp :

tactic_doc_entry

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.