Commit 2022-09-15 04:19 d1ab5252

View on Github →

chore: simp with clauses are no longer needed (#409) Some mathport syntax cleanup:

  • use simpArgs instead of [simpArg,*]
  • use dsimpArg / dsimpArgs instead of simpArg (excludes *) for consistency with core
  • remove simp', dsimp' which are no longer needed since all features exist upstream
  • mark rw_search as "skip" since it is no longer attested in mathlib
  • remove squeeze_simp, it overlaps with simp? in functionality so we'll just make one thing that does both

Estimated changes