From b429794ebc597602e40bc585a092b394fd7d9633 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Jan 2020 15:04:20 -0800 Subject: [PATCH] chore: naming convention --- src/Init/Data/List/Basic.lean | 4 ++-- src/Init/Lean/Util/WHNF.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) 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]