mathlib3
902d3ac9 - chore(tactic/rewrite_search): reuse rw_rules_p parser (#8752)

Commit

4 years ago

chore(tactic/rewrite_search): reuse rw_rules_p parser (#8752) The parser defined here is the same as `rw_rules_p`, so use it.

Author

digama0

Parents