From 1b4272821d034a2721893171f5c0d0294861753a Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 9 Jan 2025 08:01:35 +0100 Subject: [PATCH] feat: add UInt32.{lt, le} (#6591) This PR adds less-than and less-than-or-equal-to relations to `UInt32`, consistent with the other `UIntN` types. --- src/Init/Data/UInt/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean index 8a41d8df3497..081979f23a1d 100644 --- a/src/Init/Data/UInt/Basic.lean +++ b/src/Init/Data/UInt/Basic.lean @@ -159,6 +159,8 @@ def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩ def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (mod b 32).toBitVec⟩ @[extern "lean_uint32_shift_right"] def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (mod b 32).toBitVec⟩ +def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec +def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec instance : Add UInt32 := ⟨UInt32.add⟩ instance : Sub UInt32 := ⟨UInt32.sub⟩ @@ -169,6 +171,8 @@ set_option linter.deprecated false in instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩ instance : Div UInt32 := ⟨UInt32.div⟩ +instance : LT UInt32 := ⟨UInt32.lt⟩ +instance : LE UInt32 := ⟨UInt32.le⟩ @[extern "lean_uint32_complement"] def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩