summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
authorSon Ho2023-10-24 16:43:00 +0200
committerSon Ho2023-10-24 16:43:00 +0200
commitfb4fe9ec2c00f15a745ee12357e4a8f929a4dfc0 (patch)
treec88308a5011b6fd3a9ee72036ee5b236839c84b5 /backends/lean/Base/Primitives
parentce4de37c76d85ed7795f4938cf212abd31668007 (diff)
Fix minor issues
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives/Base.lean4
1 files changed, 2 insertions, 2 deletions
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 7c0fa3bb..2bd081c0 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -120,8 +120,8 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
-- MISC --
----------
-@[simp] def mem.replace (a : Type) (x : a) (_ : a) : a := x
-@[simp] def mem.replace_back (a : Type) (_ : a) (y : a) : a := y
+@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : Result a := ret x
+@[simp] def core.mem.replace_back (a : Type) (_ : a) (y : a) : Result a := ret y
/-- Aeneas-translated function -- useful to reduce non-recursive definitions.
Use with `simp [ aeneas ]` -/