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/coq/Primitives.v               | 2 +-
 backends/fstar/merge/Primitives.fst     | 2 +-
 backends/lean/Base/Primitives/Base.lean | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'backends')

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index c0056073..e6d3118f 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -67,7 +67,7 @@ Definition string := Coq.Strings.String.string.
 Definition char := Coq.Strings.Ascii.ascii.
 Definition char_of_byte := Coq.Strings.Ascii.ascii_of_byte.
 
-Definition core_mem_replace (a : Type) (x : a) (y : a) : a * (a -> a) := (x, fun x => x) .
+Definition core_mem_replace (a : Type) (x : a) (y : a) : a * a := (x, x) .
 
 Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }.
 Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }.
diff --git a/backends/fstar/merge/Primitives.fst b/backends/fstar/merge/Primitives.fst
index 6b8dbeb7..8011efa1 100644
--- a/backends/fstar/merge/Primitives.fst
+++ b/backends/fstar/merge/Primitives.fst
@@ -55,7 +55,7 @@ type string = string
 let is_zero (n: nat) : bool = n = 0
 let decrease (n: nat{n > 0}) : nat = n - 1
 
-let core_mem_replace (a : Type0) (x : a) (y : a) : a & (a -> a) = (x, (fun x -> x))
+let core_mem_replace (a : Type0) (x : a) (y : a) : a & a = (x, x)
 
 // We don't really use raw pointers for now
 type mut_raw_ptr (t : Type0) = { v : t }
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