1 parameter type

List :(->TypeType)

constructor

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

constructor

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

syntax

( build-list Ae...)

> (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 Alsn)→(Maybe A)

A:Type

ls:(List A)

n:Nat

procedure

( list-append Als1ls2)→(List A)

A:Type

ls1:(List A)

ls2:(List A)

> (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)))))