diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 9008c707b1..8e2efebdd5 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -153,11 +153,11 @@ def dropWhile (p : α → Bool) : List α → List α | true => dropWhile l | false => a::l -def find (p : α → Bool) : List α → Option α +def find? (p : α → Bool) : List α → Option α | [] => none | a::as => match p a with | true => some a - | false => find as + | false => find? as def findSome? (f : α → Option β) : List α → Option β | [] => none diff --git a/src/Init/Lean/Util/WHNF.lean b/src/Init/Lean/Util/WHNF.lean index 149b175c0a..9a3ad4c88c 100644 --- a/src/Init/Lean/Util/WHNF.lean +++ b/src/Init/Lean/Util/WHNF.lean @@ -59,7 +59,7 @@ private def toCtorIfLit : Expr → Expr private def getRecRuleFor (rec : RecursorVal) (major : Expr) : Option RecursorRule := match major.getAppFn with -| Expr.const fn _ _ => rec.rules.find $ fun r => r.ctor == fn +| Expr.const fn _ _ => rec.rules.find? $ fun r => r.ctor == fn | _ => none @[specialize] private def toCtorWhenK {m : Type → Type} [Monad m]