summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
authorSon Ho2023-11-29 15:48:07 +0100
committerSon Ho2023-11-29 15:48:07 +0100
commit5bf73730e13e51f6dc2a46f92d2ddde152c1c5d2 (patch)
tree17660fe434301e3c733623452616a55af5396d0e /tests/lean
parent3aa9c531db4e9cde25a4a149a64e3ff730ed798b (diff)
Generate the Bitwise test files
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/Bitwise.lean37
1 files changed, 37 insertions, 0 deletions
diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
new file mode 100644
index 00000000..c8538aa2
--- /dev/null
+++ b/tests/lean/Bitwise.lean
@@ -0,0 +1,37 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [bitwise]
+import Base
+open Primitives
+
+namespace bitwise
+
+/- [bitwise::shift_u32]: forward function
+ Source: 'src/bitwise.rs', lines 3:0-3:31 -/
+def shift_u32 (a : U32) : Result U32 :=
+ do
+ let t ← a >>> 16#usize
+ t <<< 16#usize
+
+/- [bitwise::shift_i32]: forward function
+ Source: 'src/bitwise.rs', lines 10:0-10:31 -/
+def shift_i32 (a : I32) : Result I32 :=
+ do
+ let t ← a >>> 16#isize
+ t <<< 16#isize
+
+/- [bitwise::xor_u32]: forward function
+ Source: 'src/bitwise.rs', lines 17:0-17:37 -/
+def xor_u32 (a : U32) (b : U32) : Result U32 :=
+ Result.ret (a ^^^ b)
+
+/- [bitwise::or_u32]: forward function
+ Source: 'src/bitwise.rs', lines 21:0-21:36 -/
+def or_u32 (a : U32) (b : U32) : Result U32 :=
+ Result.ret (a ||| b)
+
+/- [bitwise::and_u32]: forward function
+ Source: 'src/bitwise.rs', lines 25:0-25:37 -/
+def and_u32 (a : U32) (b : U32) : Result U32 :=
+ Result.ret (a &&& b)
+
+end bitwise