From 4e87d7f1734db6aa3afe56ac8aede0e1599e557d Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 23 Feb 2024 13:07:18 +1100 Subject: [PATCH] chore: rename Bool.toNat_le_one (#3469) To merge after #3457. --------- Co-authored-by: Alex Keizer --- src/Init/Data/BitVec/Bitblast.lean | 2 +- src/Init/Data/Bool.lean | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 44f8941ffa..d8296f511a 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -91,7 +91,7 @@ private theorem mod_two_pow_succ (x i : Nat) : private theorem mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toNat) < 2^(i+1) := by - have : c.toNat ≤ 1 := Bool.toNat_le_one c + have : c.toNat ≤ 1 := Bool.toNat_le c rw [Nat.pow_succ] omega diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index e77952c705..be1e924300 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -217,11 +217,13 @@ def toNat (b:Bool) : Nat := cond b 1 0 @[simp] theorem toNat_true : true.toNat = 1 := rfl -theorem toNat_le_one (c:Bool) : c.toNat ≤ 1 := by +theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by cases c <;> trivial +@[deprecated toNat_le] abbrev toNat_le_one := toNat_le + theorem toNat_lt (b : Bool) : b.toNat < 2 := - Nat.lt_succ_of_le (toNat_le_one _) + Nat.lt_succ_of_le (toNat_le _) @[simp] theorem toNat_eq_zero (b : Bool) : b.toNat = 0 ↔ b = false := by cases b <;> simp