Commit 2020-05-21 18:58 ec01a0d5

View on Github →

perf(tactic/lint/simp): speed up simp_comm linter (#2760) This is a fairly unimportant linter, but takes 35% of the linting runtime in my unscientific small-case profiling run.

Estimated changes

Modified src/algebra/euclidean_domain.lean

modified theorem euclidean_domain.xgcd_aux_rec

Modified src/data/int/gcd.lean

modified theorem nat.xgcd_aux_rec

Modified src/tactic/lint/simp.lean