max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add Option.or_some' (#5926)

Browse source 
`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).
This commit is contained in:
Violeta Hernández 2024-11-04 19:39:02 -06:00 • committed by GitHub
parent e573676db1
commit 02baaa42ff
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Data/Option/Lemmas.lean
View file

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