fix: naming convention

leanprover-community · Jun 21, 2024 · 738f4b7 · 738f4b7
1 parent 5651f64
commit 738f4b7
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean
@@ -65,7 +65,7 @@ theorem UInt8.le_iff_toNat_le_toNat {x y : UInt8} : x ≤ y ↔ x.toNat ≤ y.to
 
 theorem UInt8.lt_iff_toNat_lt_toNat {x y : UInt8} : x < y ↔ x.toNat < y.toNat := .rfl
 
-theorem UInt8.compare_eq_compare_toNat (x y : UInt8) : compare x y = compare x.toNat y.toNat := by
+theorem UInt8.compare_eq_toNat_compare_toNat (x y : UInt8) : compare x y = compare x.toNat y.toNat := by
   simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff]
 
 theorem UInt8.max_def (x y : UInt8) : max x y = if x ≤ y then y else x := rfl
@@ -152,7 +152,7 @@ theorem UInt16.le_iff_toNat_le_toNat {x y : UInt16} : x ≤ y ↔ x.toNat ≤ y.
 
 theorem UInt16.lt_iff_toNat_lt_toNat {x y : UInt16} : x < y ↔ x.toNat < y.toNat := .rfl
 
-theorem UInt16.compare_eq_compare_toNat (x y : UInt16) : compare x y = compare x.toNat y.toNat := by
+theorem UInt16.compare_eq_toNat_compare_toNat (x y : UInt16) : compare x y = compare x.toNat y.toNat := by
   simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff]
 
 theorem UInt16.max_def (x y : UInt16) : max x y = if x ≤ y then y else x := rfl
@@ -239,7 +239,7 @@ theorem UInt32.le_iff_toNat_le_toNat {x y : UInt32} : x ≤ y ↔ x.toNat ≤ y.
 
 theorem UInt32.lt_iff_toNat_lt_toNat {x y : UInt32} : x < y ↔ x.toNat < y.toNat := .rfl
 
-theorem UInt32.compare_eq_compare_toNat (x y : UInt32) : compare x y = compare x.toNat y.toNat := by
+theorem UInt32.compare_eq_toNat_compare_toNat (x y : UInt32) : compare x y = compare x.toNat y.toNat := by
   simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff]
 
 theorem UInt32.max_def (x y : UInt32) : max x y = if x ≤ y then y else x := rfl
@@ -327,7 +327,7 @@ theorem UInt64.le_iff_toNat_le_toNat {x y : UInt64} : x ≤ y ↔ x.toNat ≤ y.
 
 theorem UInt64.lt_iff_toNat_lt_toNat {x y : UInt64} : x < y ↔ x.toNat < y.toNat := .rfl
 
-theorem UInt64.compare_eq_compare_toNat (x y : UInt64) : compare x y = compare x.toNat y.toNat := by
+theorem UInt64.compare_eq_toNat_compare_toNat (x y : UInt64) : compare x y = compare x.toNat y.toNat := by
   simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff]
 
 theorem UInt64.max_def (x y : UInt64) : max x y = if x ≤ y then y else x := rfl
@@ -427,7 +427,7 @@ theorem USize.le_iff_toNat_le_toNat {x y : USize} : x ≤ y ↔ x.toNat ≤ y.to
 
 theorem USize.lt_iff_toNat_lt_toNat {x y : USize} : x < y ↔ x.toNat < y.toNat := .rfl
 
-theorem USize.compare_eq_compare_toNat (x y : USize) : compare x y = compare x.toNat y.toNat := by
+theorem USize.compare_eq_toNat_compare_toNat (x y : USize) : compare x y = compare x.toNat y.toNat := by
   simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff]
 
 theorem USize.max_def (x y : USize) : max x y = if x ≤ y then y else x := rfl