/Prelude-v16.0.0/List

Exported files:

• all:

  ∀(a : Type) → (a → Bool) → List a → Bool
  

• any:

  ∀(a : Type) → (a → Bool) → List a → Bool
  

• build:

  ∀(a : Type) → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) → List a
  

• concat:

  ∀(a : Type) → List (List a) → List a
  

• concatMap:

  ∀(a : Type) → ∀(b : Type) → (a → List b) → List a → List b
  

• default:

  ∀(a : Type) → Optional (List a) → List a
  

• drop:

  ∀(n : Natural) → ∀(a : Type) → List a → List a
  

• empty:

  ∀(a : Type) → List a
  

• filter:

  ∀(a : Type) → (a → Bool) → List a → List a
  

• fold:

  ∀(a : Type) → List a → ∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list
  

• generate:

  Natural → ∀(a : Type) → (Natural → a) → List a
  

• head:

  ∀(a : Type) → List a → Optional a
  

• index:

  Natural → ∀(a : Type) → List a → Optional a
  

• indexed:

  ∀(a : Type) → List a → List { index : Natural, value : a }
  

• iterate:

  Natural → ∀(a : Type) → (a → a) → a → List a
  

• last:

  ∀(a : Type) → List a → Optional a
  

• length:

  ∀(a : Type) → List a → Natural
  

• map:

  ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b
  

• null:

  ∀(a : Type) → List a → Bool
  

• package.dhall
• partition:

  ∀(a : Type) → (a → Bool) → List a → Partition a
  

• replicate:

  Natural → ∀(a : Type) → a → List a
  

• reverse:

  ∀(a : Type) → List a → List a
  

• shifted:

  ∀(a : Type) → List (List { index : Natural, value : a }) → List { index : Natural, value : a }
  

• take:

  ∀(n : Natural) → ∀(a : Type) → List a → List a
  

• unzip:

  ∀(a : Type) → ∀(b : Type) → List { _1 : a, _2 : b } → { _1 : List a, _2 : List b }
  

• zip:

  ∀(a : Type) → List a → ∀(b : Type) → List b → List { _1 : a, _2 : b }