summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Scalar.lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean63
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