Add tests for the builtin definitions

tests/lean/Builtin.lean

@@ -0,0 +1,55 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [builtin]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace builtin
+
+/- [builtin::clone_bool]:
+   Source: 'tests/src/builtin.rs', lines 5:0-7:1 -/
+def clone_bool (x : Bool) : Result Bool :=
+  Result.ok (core.clone.impls.CloneBool.clone x)
+
+/- [builtin::clone_u32]:
+   Source: 'tests/src/builtin.rs', lines 9:0-11:1 -/
+def clone_u32 (x : U32) : Result U32 :=
+  Result.ok (core.clone.impls.CloneU32.clone x)
+
+/- [builtin::into_from]:
+   Source: 'tests/src/builtin.rs', lines 13:0-15:1 -/
+def into_from
+  {T : Type} {U : Type} (coreconvertFromInst : core.convert.From U T) (x : T) :
+  Result U
+  :=
+  core.convert.IntoFrom.into coreconvertFromInst x
+
+/- [builtin::into_same]:
+   Source: 'tests/src/builtin.rs', lines 17:0-19:1 -/
+def into_same {T : Type} (x : T) : Result T :=
+  core.convert.IntoFrom.into (core.convert.FromSame T) x
+
+/- [builtin::from_same]:
+   Source: 'tests/src/builtin.rs', lines 21:0-23:1 -/
+def from_same {T : Type} (x : T) : Result T :=
+  Result.ok (core.convert.FromSame.from_ x)
+
+/- [builtin::copy]:
+   Source: 'tests/src/builtin.rs', lines 25:0-27:1 -/
+def copy
+  {T : Type} (coremarkerCopyInst : core.marker.Copy T) (x : T) : Result T :=
+  Result.ok x
+
+/- [builtin::u32_from_le_bytes]:
+   Source: 'tests/src/builtin.rs', lines 29:0-31:1 -/
+def u32_from_le_bytes (x : Array U8 4#usize) : Result U32 :=
+  Result.ok (core.num.U32.from_le_bytes x)
+
+/- [builtin::u32_to_le_bytes]:
+   Source: 'tests/src/builtin.rs', lines 33:0-35:1 -/
+def u32_to_le_bytes (x : U32) : Result (Array U8 4#usize) :=
+  Result.ok (core.num.U32.to_le_bytes x)
+
+end builtin

tests/src/builtin.rs

@@ -0,0 +1,35 @@
+//@[!lean] skip
+//! This file uses a list of builtin definitions, to make sure they are properly
+//! detected and mapped to definitions in the standard library.
+
+fn clone_bool(x: bool) -> bool {
+    x.clone()
+}
+
+fn clone_u32(x: u32) -> u32 {
+    x.clone()
+}
+
+fn into_from<T, U: From<T>>(x: T) -> U {
+    x.into()
+}
+
+fn into_same<T>(x: T) -> T {
+    x.into()
+}
+
+fn from_same<T>(x: T) -> T {
+    T::from(x)
+}
+
+fn copy<T: Copy>(x: &T) -> T {
+    *x
+}
+
+fn u32_from_le_bytes(x: [u8; 4]) -> u32 {
+    u32::from_le_bytes(x)
+}
+
+fn u32_to_le_bytes(x: u32) -> [u8; 4] {
+    x.to_le_bytes()
+}