@[deprecated Option.toList_some]

theorem Option.to_list_some {α : Type u_1} (a : α) : Option.toList (some a) = [a]

Alias of Option.toList_some.

@[deprecated Option.toList_none]

theorem Option.to_list_none (α : Type u_1) : Option.toList none = []

Alias of Option.toList_none.