From 58ddeedced1d1a6b44baca06c62b1e4d01fa2233 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Mar 2020 08:30:20 -0800
Subject: [PATCH] feat: add `List.replace`

---
 src/Init/Data/List/Basic.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 8e2efebdd5..0a71a5396b 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -165,6 +165,12 @@ def findSome? (f : α → Option β) : List α → Option β
   | some b => some b
   | none   => findSome? as
 
+def replace [HasBeq α] : List α → α → α → List α
+| [],    _, _ => []
+| a::as, b, c => match a == b with
+  | true  => c::as
+  | flase => a :: (replace as b c)
+
 def elem [HasBeq α] (a : α) : List α → Bool
 | []    => false
 | b::bs => match a == b with