From 02baaa42ffb66adf6e1ee1c2faed6dfd9fb3ff26 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Mon, 4 Nov 2024 19:39:02 -0600 Subject: [PATCH] feat: add `Option.or_some'` (#5926) `o.or (some a) = o.getD a`. As discussed on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/a.2Eor.20.28some.20b.29.20.3D.20a.2EgetD.20b/near/472785093). --- src/Init/Data/Option/Lemmas.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index 786bb371c7..d7f07a3db6 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -374,9 +374,15 @@ end choice -- See `Init.Data.Option.List` for lemmas about `toList`. -@[simp] theorem or_some : (some a).or o = some a := rfl +@[simp] theorem some_or : (some a).or o = some a := rfl @[simp] theorem none_or : none.or o = o := rfl +@[deprecated some_or (since := "2024-11-03")] theorem or_some : (some a).or o = some a := rfl + +/-- This will be renamed to `or_some` once the existing deprecated lemma is removed. -/ +@[simp] theorem or_some' {o : Option α} : o.or (some a) = o.getD a := by + cases o <;> rfl + theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by cases o <;> rfl