Documentation

Mathlib.Init.Data.List.Instances

Decidable and Monad instances for List not (yet) in Batteries #

Equations
@[simp]
theorem List.pure_def {α : Type u} (a : α) :
pure a = [a]
Equations