Def CmpUsing

Modification history

2022-11-13 23:39

Mathlib/Init/Data/Ordering/Basic.lean

fix: naming convention for `cmp` and `cmpUsing` (#589) …

Deleted CmpUsing View on Github →

2022-11-11 02:27

Mathlib/Init/Data/Ordering/Basic.lean

feat: Init.Data.Ordering.Basic (#568)

Added CmpUsing View on Github →