mathlib documentation


Generating a list of rewrites to use as steps in rewrite search. #

Use this attribute to make rewrite_search use this definition during search.

Collect rewrite rules to use from the environment.

Get all rewrites that start at the given expression and use one of the given rewrite rules.