mathlib
893ce8b6 - feat(tactic/norm_fin): tactic for normalizing `fin n` expressions (#5820)

Commit
4 years ago
feat(tactic/norm_fin): tactic for normalizing `fin n` expressions (#5820) This is based on #5791, with a new implementation using the `normalize_fin` function. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Author
Parents
Loading