From ce7bd25534cb732339699c062049f57c493bedc5 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Thu, 20 Jun 2024 09:53:18 -0400 Subject: [PATCH] fix: long lines --- Batteries/Data/UInt.lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean index ddb6ca8783..2c2b18bcad 100644 --- a/Batteries/Data/UInt.lean +++ b/Batteries/Data/UInt.lean @@ -65,7 +65,8 @@ 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_toNat_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 +153,8 @@ 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_toNat_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 +241,8 @@ 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_toNat_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 +330,8 @@ 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_toNat_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 +431,8 @@ 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_toNat_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