mathlib
df84064e - fix(tactic/clear): don't use rb_map unnecessarily (#2325)

Commit
5 years ago
fix(tactic/clear): don't use rb_map unnecessarily (#2325) The `clear_dependent` tactic seems to unnecessarily convert `list` back and forth to an `rb_map`, for no purpose, and this makes the internal tactic unnecessarily difficult to call. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Jannis Limperg <jannis@limperg.de> Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading