Update the tests for External

1 files changed, 75 insertions, 0 deletions

diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index acdb09dc..c7c9f9db 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -465,6 +465,81 @@ let i64_shr #ty = scalar_shr #I64 #ty
 let i128_shr #ty = scalar_shr #I128 #ty
 let isize_shr #ty = scalar_shr #Isize #ty
 
+(*** core *)
+
+/// Trait declaration: [core::clone::Clone]
+noeq type core_clone_Clone (self : Type0) = {
+  clone : self → result self
+}
+
+let core_clone_impls_CloneBool_clone (b : bool) : bool = b
+
+let core_clone_CloneBool : core_clone_Clone bool = {
+  clone = fun b -> Ok (core_clone_impls_CloneBool_clone b)
+}
+
+let core_clone_impls_CloneUsize_clone (x : usize) : usize = x
+let core_clone_impls_CloneU8_clone (x : u8) : u8 = x
+let core_clone_impls_CloneU16_clone (x : u16) : u16 = x
+let core_clone_impls_CloneU32_clone (x : u32) : u32 = x
+let core_clone_impls_CloneU64_clone (x : u64) : u64 = x
+let core_clone_impls_CloneU128_clone (x : u128) : u128 = x
+
+let core_clone_impls_CloneIsize_clone (x : isize) : isize = x
+let core_clone_impls_CloneI8_clone (x : i8) : i8 = x
+let core_clone_impls_CloneI16_clone (x : i16) : i16 = x
+let core_clone_impls_CloneI32_clone (x : i32) : i32 = x
+let core_clone_impls_CloneI64_clone (x : i64) : i64 = x
+let core_clone_impls_CloneI128_clone (x : i128) : i128 = x
+
+let core_clone_CloneUsize : core_clone_Clone usize = {
+  clone = fun x -> Ok (core_clone_impls_CloneUsize_clone x)
+}
+
+let core_clone_CloneU8 : core_clone_Clone u8 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU8_clone x)
+}
+
+let core_clone_CloneU16 : core_clone_Clone u16 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU16_clone x)
+}
+
+let core_clone_CloneU32 : core_clone_Clone u32 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU32_clone x)
+}
+
+let core_clone_CloneU64 : core_clone_Clone u64 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU64_clone x)
+}
+
+let core_clone_CloneU128 : core_clone_Clone u128 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU128_clone x)
+}
+
+let core_clone_CloneIsize : core_clone_Clone isize = {
+  clone = fun x -> Ok (core_clone_impls_CloneIsize_clone x)
+}
+
+let core_clone_CloneI8 : core_clone_Clone i8 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI8_clone x)
+}
+
+let core_clone_CloneI16 : core_clone_Clone i16 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI16_clone x)
+}
+
+let core_clone_CloneI32 : core_clone_Clone i32 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI32_clone x)
+}
+
+let core_clone_CloneI64 : core_clone_Clone i64 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI64_clone x)
+}
+
+let core_clone_CloneI128 : core_clone_Clone i128 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
+}
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]