Commit 2023-01-25 10:48 9a21a9e6

View on Github →

Feat: port Part.toOption_isSome and Part.toOption_isNone (#1520) This is the forward-port of leanprover-community/mathlib#18153

Estimated changes

added theorem Part.toOption_isNone
added theorem Part.toOption_isSome