@[simp]

theorem Option.mem_toList {α : Type u_1} {a : α} {o : Option α} : a ∈ o.toList ↔ a ∈ o

@[simp]

theorem Option.forIn'_none {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (b : β) (f : (a : α) → a ∈ none → β → m (ForInStep β)) : forIn' none b f = pure b

@[simp]

theorem Option.forIn'_some {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (a : α) (b : β) (f : (a' : α) → a' ∈ some a → β → m (ForInStep β)) : forIn' (some a) b f = do let r ← f a ⋯ b pure r.value

@[simp]

theorem Option.forIn_none {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (b : β) (f : α → β → m (ForInStep β)) : forIn none b f = pure b

@[simp]

theorem Option.forIn_some {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (a : α) (b : β) (f : α → β → m (ForInStep β)) : forIn (some a) b f = do let r ← f a b pure r.value

@[simp]

theorem Option.forIn'_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)) : forIn' o.toList b f = forIn' o b fun (a : α) (m : a ∈ o) (b : β) => f a ⋯ b

@[simp]

theorem Option.forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) : forIn o.toList b f = forIn o b f

@[simp]

theorem Option.foldlM_toList {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_1} [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) : List.foldlM f a o.toList = o.elim (pure a) fun (b : β) => f a b

@[simp]

theorem Option.foldrM_toList {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_1} [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) : List.foldrM f a o.toList = o.elim (pure a) fun (b : β) => f b a

@[simp]

theorem Option.foldl_toList {β : Type u_1} {α : Type u_2} (o : Option β) (a : α) (f : α → β → α) : List.foldl f a o.toList = o.elim a fun (b : β) => f a b

@[simp]

theorem Option.foldr_toList {β : Type u_1} {α : Type u_2} (o : Option β) (a : α) (f : β → α → α) : List.foldr f a o.toList = o.elim a fun (b : β) => f b a

@[simp]

theorem Option.pairwise_toList {α : Type u_1} {P : α → α → Prop} {o : Option α} : List.Pairwise P o.toList

@[simp]

theorem Option.head?_toList {α : Type u_1} {o : Option α} : o.toList.head? = o