From 8719c17f1a363c0463d74b90e558b2aaa24645d6 Mon Sep 17 00:00:00 2001
From: Son HO
Date: Sat, 22 Jun 2024 15:07:14 +0200
Subject: Do some cleanup in the Lean backend (#257)

---
 backends/lean/Base/Primitives/Base.lean | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

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

diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index c9237e65..63fbd8c0 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -134,18 +134,16 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ok x } :=
 -- MISC --
 ----------
 
--- This acts like a swap effectively in a functional pure world.
--- We return the old value of `dst`, i.e. `dst` itself.
--- The new value of `dst` is `src`.
-@[simp] def core.mem.replace (a : Type) (dst : a) (src : a) : a × a := (dst, src)
-/- [core::option::Option::take] -/
-@[simp] def Option.take (T: Type) (self: Option T): Option T × Option T := (self, .none)
-/- [core::mem::swap] -/
-@[simp] def core.mem.swap (T: Type) (a b: T): T × T := (b, a)
-
-/-- Aeneas-translated function -- useful to reduce non-recursive definitions.
- Use with `simp [ aeneas ]` -/
-register_simp_attr aeneas
+instance SubtypeBEq [BEq α] (p : α → Prop) : BEq (Subtype p) where
+  beq v0 v1 := v0.val == v1.val
+
+instance SubtypeLawfulBEq [BEq α] (p : α → Prop) [LawfulBEq α] : LawfulBEq (Subtype p) where
+  eq_of_beq {a b} h := by cases a; cases b; simp_all [BEq.beq]
+  rfl := by intro a; cases a; simp [BEq.beq]
+
+------------------------------
+---- Misc Primitives Types ---
+------------------------------
 
 -- We don't really use raw pointers for now
 structure MutRawPtr (T : Type) where
-- 
cgit v1.2.3