mathlib
f1b0402a - feat(tactic/core + test/list_summands): a function extracting a list of summands from an expression (#14617)

Commit
3 years ago
feat(tactic/core + test/list_summands): a function extracting a list of summands from an expression (#14617) This meta def is used in #13483, where `move_add` is defined. A big reason for splitting these 5 lines off the main PR is that they are not in a leaf of the import hierarchy: this hopefully saves lots of CI time, when doing trivial changes to the main PR. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading