diff options
author | Son Ho | 2024-04-25 16:07:56 +0200 |
---|---|---|
committer | Son Ho | 2024-04-25 16:07:56 +0200 |
commit | 078b7f59ddfcb12a7b4c69f0a51bfd57cb391ddf (patch) | |
tree | ed45664329e24d1773be6c8bcaf827e2adbd3f65 /tests/fstar/hashmap | |
parent | 1728dced8484befe35ef61fdf4ccd62b93fbb19d (diff) | |
parent | a3e38d5f47e4780768902e49e28e471e38efd40a (diff) |
Merge branch 'main' into core-option-unwrap
Diffstat (limited to 'tests/fstar/hashmap')
-rw-r--r-- | tests/fstar/hashmap/Primitives.fst | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst index acdb09dc..c7c9f9db 100644 --- a/tests/fstar/hashmap/Primitives.fst +++ b/tests/fstar/hashmap/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] |