Commit 2025-08-30 15:25 45948293

View on Github →

style: prefer some/none over .some/.none (#27896) The notation .some and .none are very useful when working with other inductive types such as LOption which have fields names some and/or none. But for Option, we prefer to simply write some/none. [#mathlib4 > style: `.some`/`.none` vs `some`/`none`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/style.3A.20.60.2Esome.60.2F.60.2Enone.60.20vs.20.60some.60.2F.60none.60)

Estimated changes