summaryrefslogtreecommitdiff
path: root/backends/fstar/merge/Primitives.fst
diff options
context:
space:
mode:
Diffstat (limited to 'backends/fstar/merge/Primitives.fst')
-rw-r--r--backends/fstar/merge/Primitives.fst2
1 files changed, 1 insertions, 1 deletions
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 }