summaryrefslogtreecommitdiff
path: root/tests/lean/Bitwise.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Bitwise.lean')
-rw-r--r--tests/lean/Bitwise.lean8
1 files changed, 4 insertions, 4 deletions
diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
index 23ec66b4..8884d309 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 >>> 16#usize
- t <<< 16#usize
+ let t ← a >>> 16usize
+ t <<< 16usize
/- [bitwise::shift_i32]:
Source: 'tests/src/bitwise.rs', lines 12:0-12:31 -/
def shift_i32 (a : I32) : Result I32 :=
do
- let t ← a >>> 16#isize
- t <<< 16#isize
+ let t ← a >>> 16isize
+ t <<< 16isize
/- [bitwise::xor_u32]:
Source: 'tests/src/bitwise.rs', lines 19:0-19:37 -/