Stdlib.Data.List
Contents
open import Stdlib.Data.List.Base public
head : {A : Type} → List A → ASource#
𝒪(1). Partial function that returns the first element of a List.
terminating transpose : {A : Type} → List (List A) → List (List A)Source#
𝒪(𝓃 * 𝓂). Partial function that transposes a List of Lists interpreted as a matrix.
