diff options
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 9eb5a794..b8d93d30 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -1409,4 +1409,67 @@ def core.num.I32.leading_zeros (x : I32) : U32 := sorry def core.num.I64.leading_zeros (x : I64) : U32 := sorry def core.num.I128.leading_zeros (x : I128) : U32 := sorry +-- Clone +def core.clone.impls.CloneUsize.clone (x : Usize) : Usize := x +def core.clone.impls.CloneU8.clone (x : U8) : U8 := x +def core.clone.impls.CloneU16.clone (x : U16) : U16 := x +def core.clone.impls.CloneU32.clone (x : U32) : U32 := x +def core.clone.impls.CloneU64.clone (x : U64) : U64 := x +def core.clone.impls.CloneU128.clone (x : U128) : U128 := x + +def core.clone.impls.CloneIsize.clone (x : Isize) : Isize := x +def core.clone.impls.CloneI8.clone (x : I8) : I8 := x +def core.clone.impls.CloneI16.clone (x : I16) : I16 := x +def core.clone.impls.CloneI32.clone (x : I32) : I32 := x +def core.clone.impls.CloneI64.clone (x : I64) : I64 := x +def core.clone.impls.CloneI128.clone (x : I128) : I128 := x + +def core.clone.CloneUsize : core.clone.Clone Usize := { + clone := fun x => ok (core.clone.impls.CloneUsize.clone x) +} + +def core.clone.CloneU8 : core.clone.Clone U8 := { + clone := fun x => ok (core.clone.impls.CloneU8.clone x) +} + +def core.clone.CloneU16 : core.clone.Clone U16 := { + clone := fun x => ok (core.clone.impls.CloneU16.clone x) +} + +def core.clone.CloneU32 : core.clone.Clone U32 := { + clone := fun x => ok (core.clone.impls.CloneU32.clone x) +} + +def core.clone.CloneU64 : core.clone.Clone U64 := { + clone := fun x => ok (core.clone.impls.CloneU64.clone x) +} + +def core.clone.CloneU128 : core.clone.Clone U128 := { + clone := fun x => ok (core.clone.impls.CloneU128.clone x) +} + +def core.clone.CloneIsize : core.clone.Clone Isize := { + clone := fun x => ok (core.clone.impls.CloneIsize.clone x) +} + +def core.clone.CloneI8 : core.clone.Clone I8 := { + clone := fun x => ok (core.clone.impls.CloneI8.clone x) +} + +def core.clone.CloneI16 : core.clone.Clone I16 := { + clone := fun x => ok (core.clone.impls.CloneI16.clone x) +} + +def core.clone.CloneI32 : core.clone.Clone I32 := { + clone := fun x => ok (core.clone.impls.CloneI32.clone x) +} + +def core.clone.CloneI64 : core.clone.Clone I64 := { + clone := fun x => ok (core.clone.impls.CloneI64.clone x) +} + +def core.clone.CloneI128 : core.clone.Clone I128 := { + clone := fun x => ok (core.clone.impls.CloneI128.clone x) +} + end Primitives |