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/fstar/merge/Primitives.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends/fstar') 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 } -- cgit v1.2.3