mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast`

Open YaelDillies opened this issue 1 year ago • 4 comments
trafficstars

This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy.

Reduce the diff of #11203


  • [x] depends on: #11528
  • [x] depends on: #11552
  • [ ] depends on: #11637

Open in Gitpod

YaelDillies avatar Mar 19 '24 08:03 YaelDillies