mathlib3
7907f8f3 - feat(tactic/tidy): include norm_cast in tidy (#2063)

Commit
5 years ago
feat(tactic/tidy): include norm_cast in tidy (#2063) * feat(tactic/tidy): include norm_cast in tidy * Update src/tactic/core.lean Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading