Documentation

Batteries.Data.Option.Lemmas

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

Alias of Option.toList_some.

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

Alias of Option.toList_none.