mathlib3
dcbc719b - fix(tactic/squeeze): compatibility with `simp [<-...]` (#1923)

Commit
6 years ago
fix(tactic/squeeze): compatibility with `simp [<-...]` (#1923) * Add polyfills to `squeeze_simp` which should ensure compatibility with Lean 3.4 and 3.5 * Use `decode_simp_arg_list` so `squeeze_simp` doesn't have to pattern-match (Except of course for the polyfill `has_to_tactic_format simp_arg_type` instance...) * Reword comment for `erase_simp_args` Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading