From e51d892fc2d2454cf45dc1bc26dd926a189b0ac0 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 7 Aug 2022 16:11:10 -0400 Subject: [PATCH] feat: implement USize.toUInt64 model --- src/Init/Prelude.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 96edf7c502..338d31a572 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3203,7 +3203,16 @@ This is lossless because `USize.size` is either `2^32` or `2^64`. This function is overridden with a native implementation. -/ @[extern "lean_usize_to_uint64"] -opaque USize.toUInt64 (u : USize) : UInt64 +def USize.toUInt64 (u : USize) : UInt64 where + val := { + val := u.val.val + isLt := + let ⟨n, h⟩ := u + show LT.lt n _ from + match USize.size, usize_size_eq, h with + | _, Or.inl rfl, h => Nat.lt_trans h (by decide) + | _, Or.inr rfl, h => h + } /-- An opaque hash mixing operation, used to implement hashing for tuples. -/ @[extern "lean_uint64_mix_hash"]