mathlib3
bc278b7e - fix(tactic/apply_rules): fix stuck metavariable bug (#3451)

Commit
6 years ago
fix(tactic/apply_rules): fix stuck metavariable bug (#3451) `apply_rules` had the same bug `solve_by_elim` used to suffer from: applying a lemma once would fix its arguments, and prevent it from being applied a second time with different arguments. This essentially ports over the fix from `solve_by_elim`: rather than carrying around a `list expr`, we carry a `list (tactic expr)` and generate on demand. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Author
Parents
Loading