From d9ace7d5f1968f26b586fb712c725b2ce51086f8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 21:50:11 +0100
Subject: Fix the models for core::mem::replace

---
 backends/lean/Base/Primitives/Base.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 321c39a8..3d70c84a 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -120,7 +120,7 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
 -- MISC --
 ----------
 
-@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a × (a → a) := (x, λ x => x)
+@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a × a := (x, x)
 
 /-- Aeneas-translated function -- useful to reduce non-recursive definitions.
  Use with `simp [ aeneas ]` -/
-- 
cgit v1.2.3