From f35aba375757db99d2dc6ac2b11b9eb1e437b420 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 11:58:35 +0200
Subject: Add definitions in for the Lean Primitives library

---
 backends/lean/Base/Primitives/Alloc.lean | 37 ++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 backends/lean/Base/Primitives/Alloc.lean

(limited to 'backends/lean/Base/Primitives/Alloc.lean')

diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
new file mode 100644
index 00000000..0580421f
--- /dev/null
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -0,0 +1,37 @@
+import Lean
+import Base.Primitives.Base
+import Base.Primitives.CoreOpsDeref
+
+open Primitives
+open Result
+
+namespace alloc
+
+namespace boxed -- alloc.boxed
+
+namespace Box -- alloc.boxed.Box
+
+def deref (T : Type) (x : T) : Result T := ret x
+def deref_mut (T : Type) (x : T) : Result T := ret x
+def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x
+
+/-- Trait instance -/
+def coreOpsDerefInst (Self : Type) :
+  core.ops.deref.Deref Self := {
+  Target := Self
+  deref := deref Self
+}
+
+/-- Trait instance -/
+def coreOpsDerefMutInst (Self : Type) :
+  core.ops.deref.DerefMut Self := {
+  derefInst := coreOpsDerefInst Self
+  deref_mut := deref_mut Self
+  deref_mut_back := deref_mut_back Self
+}
+
+end Box -- alloc.boxed.Box
+
+end boxed -- alloc.boxed
+
+end alloc
-- 
cgit v1.2.3