Additional Option functions and lemmas

def Option.mapD {α : Type u_1} {β : Sort u_2} (f : α → β) (default : β) : Option α → β

Equations

• Option.mapD f default (some a) = f a
• Option.mapD f default none = default

@[simp]

theorem Option.mapD_some {α : Type u_1} {β : Sort u_2} (f : α → β) (default : β) (a : α) : mapD f default (some a) = f a

@[simp]

theorem Option.mapD_none {α : Type u_1} {β : Sort u_2} (f : α → β) (default : β) : mapD f default none = default