summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base/Primitives/Base.lean2
1 files changed, 1 insertions, 1 deletions
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 ]` -/