List.reduceOption_cons_of_none
theorem List.reduceOption_cons_of_none :
∀ {α : Type u_1} (l : List (Option α)), (none :: l).reduceOption = l.reduceOption
The theorem `List.reduceOption_cons_of_none` states that for any list of optional values `l` of any type `α`, the operation of reducing the list by eliminating `none` values and replacing `some a` values with `a` remains unaffected by prepending a `none` to this list. In other words, for any list `l`, `List.reduceOption (none :: l)` equals `List.reduceOption l`.
More concisely: For any list `l` of optional values and any type `α`, `List.reduceOption (none :: l) = List.reduceOption l`.
|
List.reduceOption_cons_of_some
theorem List.reduceOption_cons_of_some :
∀ {α : Type u_1} (x : α) (l : List (Option α)), (some x :: l).reduceOption = x :: l.reduceOption
The theorem `List.reduceOption_cons_of_some` states that for any type `α`, any element `x` of type `α` and any list `l` of optional `α`, when the `reduceOption` function is applied to a list that starts with `some x` and followed by `l`, it results in a list that starts with `x` and followed by the list obtained by applying the `reduceOption` function to `l`. Essentially, it says that the `reduceOption` function removes the `some` wrapper from the head of the list and operates independently on the rest of the list.
More concisely: For any type `α` and any `x : α` and optional list `ls : option list α`, `List.reduceOption x (some x :: ls) = x :: List.reduceOption ls`.
|