a.or (some b) = a.getD b

Stream: Is there code for X?

[Violeta Hernández]

What it says in the title.

[Violeta Hernández]

theorem Option.or_some_right {α : Type*} (a : Option α) (b : α) :
    a.or (some b) = a.getD b := by
  cases a <;> rfl

[Kim Morrison]

Probably could just be called or_some.

[Kim Morrison]

But yes, seems plausible. I guess we already have simp lemmas for the other three cases?

[Violeta Hernández]

docs#Option.or_some is already a different lemma

[Violeta Hernández]

Yep, we seem to have the other three

[Violeta Hernández]

docs#Option.none_or and docs#Option.or_none

[Kim Morrison]

Ugh, okay or_some should be renamed to some_or, and then your suggestion can become some_or.

[Kim Morrison]

Would you be able to PR that?

[Violeta Hernández]

Sure, just give me a couple of hours

[Violeta Hernández]

(I also still have to PR the pmap lemma)

[Kim Morrison]

If we wanted to be really conservative we would first rename or_some, add a deprecation, and then only add the new lemma (at least) one release later.

[Kim Morrison]

Actually, lets do that...

If you could do the rename, but for now add the new lemma as or_some', with a doc-string saying that it will be renamed to or_some once the existing deprecation is removed.

[Kim Morrison]

Painful, I realise. :-)

[Kim Morrison]

Thank you!

[Damiano Testa]

To remember about removing the prime, you could add an (untested) assert_exists Option.or_some next to or_some' so that once the deprecated lemma is removed, you'll get a warning.

[Violeta Hernández]

#5926

[Violeta Hernández]

Is alias not available in core?

[Violeta Hernández]

(also, how do I link a core PR?)

[Yaël Dillies]

lean4#5926

[Yaël Dillies]

alias is from batteries