On this page:
List
nil
cons
build-list
list-ref
list-append
8.12

3.7 List🔗ℹ

This library defines the datatype List and several functions on them.

1 parameter type

List : (-> Type Type)

constructor

nil : (-> (A : Type) (List A))

constructor

cons : (-> (A : Type) (a : A) (-> (List A) (List A)))

The polymorphic list datatype.

syntax

(build-list A e ...)

A form for iterated application of cons.

Examples:
> (build-list Nat)

(nil (Nat))

> (build-list Nat z)

(cons (Nat) (z) (nil (Nat)))

> (build-list Nat z (s z))

(cons (Nat) (z) (cons (Nat) (s (z)) (nil (Nat))))

procedure

(list-ref A ls n)  (Maybe A)

  A : Type
  ls : (List A)
  n : Nat
Returns the nth element of ls in the Maybe monad.

procedure

(list-append A ls1 ls2)  (List A)

  A : Type
  ls1 : (List A)
  ls2 : (List A)
Returns the nth element of ls in the Maybe monad.

Examples:
> (list-append Nat (nil Nat) (nil Nat))

(nil (Nat))

> (list-append Nat (build-list Nat z (s z)) (build-list Nat (s z)))

(cons (Nat) (s (z)) (cons (Nat) (z) (cons (Nat) (s (z)) (nil (Nat)))))