From bd5c6683472f93a7c419ec3c294ca3da158aaf2a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Nov 2020 12:34:40 -0800 Subject: [PATCH] feat: add helper functions for new `Prelude.lean` --- src/Init/Data/UInt.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean index 62c4f7bc6d..16e41d00e2 100644 --- a/src/Init/Data/UInt.lean +++ b/src/Init/Data/UInt.lean @@ -362,3 +362,24 @@ instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b theorem USize.modnLt {m : Nat} : ∀ (u : USize), m > 0 → USize.toNat (u %ₙ m) < m | ⟨u⟩, h => Fin.modnLt u h + +theorem usizeSzEq : usizeSz = 4294967296 ∨ usizeSz = 18446744073709551616 := + show (2 : Nat) ^ System.Platform.numBits = 4294967296 ∨ (2 : Nat) ^ System.Platform.numBits = 18446744073709551616 from + match System.Platform.numBits, System.Platform.numBitsEq with + | _, Or.inl rfl => Or.inl (decide! : (2 : Nat) ^ 32 = 4294967296) + | _, Or.inr rfl => Or.inr (decide! : (2 : Nat) ^ 64 = 18446744073709551616) + +@[extern "lean_usize_of_nat"] +def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize := { + val := { + val := n, + isLt := match usizeSz, usizeSzEq with + | _, Or.inl rfl => h + | _, Or.inr rfl => Nat.ltTrans h (decide! : Less 4294967296 18446744073709551616) + } +} + +@[extern "lean_usize_of_nat"] +def USize.ofNatCore (n : @& Nat) (h : n < usizeSz) : USize := { + val := { val := n, isLt := h } +}