def cons (α : Type) (a : α) (as : List α) : List α :=
List.cons a as
#check cons Nat -- Nat → List Nat → List Nat
#check cons Bool -- Bool → List Bool → List Bool
#check cons -- (α : Type) → α → List α → List α类似于宏/多态，函数的具体类型和实现随参数而变化。