summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base/Primitives.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 808c1461..14f5971e 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -656,7 +656,7 @@ def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec
-- MISC --
----------
-@[simp] def mem.replace_fwd (a : Type) (x : a) (_ : a) : a := x
+@[simp] def mem.replace (a : Type) (x : a) (_ : a) : a := x
@[simp] def mem.replace_back (a : Type) (_ : a) (y : a) : a := y
/-- Aeneas-translated function -- useful to reduce non-recursive definitions.