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)