Commit 2022-11-13 23:39 c1ee6358

View on Github →

fix: naming convention for cmp and cmpUsing (#589) according to https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/naming.20conventions/near/309189032

Estimated changes

deleted def Cmp
deleted def CmpUsing
added def cmp
added def cmpUsing