def List.ofOption {α : Type u_1} : Option α → List α

Equations

• List.ofOption none = []
• List.ofOption (some x_1) = [x_1]

def List.consOption {α : Type u_1} : Option α → List α → List α

Equations

• none ::ₒ x✝ = x✝
• some x_2 ::ₒ x✝ = x_2 :: x✝

def «term_::ₒ_» : Lean.TrailingParserDescr

Equations

• «term_::ₒ_» = Lean.ParserDescr.trailingNode `«term_::ₒ_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::ₒ ") (Lean.ParserDescr.cat `term 67))

@[simp]

theorem List.ofOption_none {α : Type u_1} : ofOption none = []

@[simp]

theorem List.ofOption_some {α : Type u_1} (x : α) : ofOption (some x) = [x]

@[simp]

theorem List.consOption_none {α : Type u_1} (xs : List α) : none ::ₒ xs = xs

@[simp]

theorem List.consOption_some {α : Type u_1} (x : α) (xs : List α) : some x ::ₒ xs = x :: xs

@[simp]

theorem List.ofOption_append {α : Type u_1} (opt : Option α) (xs : List α) : ofOption opt ++ xs = opt ::ₒ xs

@[simp]

theorem List.consOption_append {α : Type u_1} (opt : Option α) (xs ys : List α) : opt ::ₒ xs ++ ys = opt ::ₒ (xs ++ ys)

@[simp]

theorem List.consOption_nil {α : Type u_1} (opt : Option α) : opt ::ₒ [] = ofOption opt