Commit 2022-10-26 09:33 f64a355f

View on Github →

feat: port Data.Option.Defs (#504)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem Option.mem_toList

Modified Mathlib/Data/Option/Basic.lean

modified theorem Option.lift_or_get_none_left

modified theorem Option.lift_or_get_none_right

Modified Mathlib/Data/Option/Defs.lean

added def Option.decidableEqNone

added def Option.iget

added theorem Option.iget_some

added theorem Option.is_none_iff_eq_none

deleted def Option.lift_or_get

deleted def Option.melim

added theorem Option.mem_some_iff

added theorem Option.mem_toList

deleted def Option.mgetD

deleted def Option.mmap.{u,