From d85d160ae9736f50d9c043b411c5a831f1fbb964 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:35 +0200
Subject: Revert "Regenerate the tests"

This reverts commit cd5542fc82edee11181a43e3a342a2567c929e7e.
---
 tests/lean/Bitwise.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tests/lean/Bitwise.lean')

diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
index 8884d309..23ec66b4 100644
--- a/tests/lean/Bitwise.lean
+++ b/tests/lean/Bitwise.lean
@@ -9,15 +9,15 @@ namespace bitwise
    Source: 'tests/src/bitwise.rs', lines 5:0-5:31 -/
 def shift_u32 (a : U32) : Result U32 :=
   do
-  let t ← a >>> 16usize
-  t <<< 16usize
+  let t ← a >>> 16#usize
+  t <<< 16#usize
 
 /- [bitwise::shift_i32]:
    Source: 'tests/src/bitwise.rs', lines 12:0-12:31 -/
 def shift_i32 (a : I32) : Result I32 :=
   do
-  let t ← a >>> 16isize
-  t <<< 16isize
+  let t ← a >>> 16#isize
+  t <<< 16#isize
 
 /- [bitwise::xor_u32]:
    Source: 'tests/src/bitwise.rs', lines 19:0-19:37 -/
-- 
cgit v1.2.3