feat: add List.replace

This commit is contained in:
Leonardo de Moura 2020-03-02 08:30:20 -08:00
parent 88dc110260
commit 58ddeedced

View file

@ -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