Def cmpUsing

Modification history

2022-11-13 23:39
Mathlib/Init/Data/Ordering/Basic.lean
fix: naming convention for `cmp` and `cmpUsing` (#589) …
Added cmpUsingView on Github →