@[reducible, inline]

abbrev NonEmptyList (α : Type u_1) : Type u_1

Equations

• NonEmptyList α = { l : List α // l ≠ [] }

@[reducible, inline]

abbrev NonEmptyList.mk {α : Type} (x : α) (xs : List α) : NonEmptyList α

Equations

• x ::₁ xs = ⟨x :: xs, ⋯⟩

@[reducible, inline]

abbrev NonEmptyList.toList {α : Type} : NonEmptyList α → List α

Equations

• x✝.toList = ↑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))