next up previous contents index
Next: Primitive Recursive Functions Up: Simulating Lambda--prl Constructs Previous: Logical Operators


The hd and tl built-in functions of Lambda--prl do not exist in Nuprl . They can be simulated with the following definitions.

    hd(<a:list>)==list_ind(<a>; "?"; h,t,v.h)
    tl(<a:list>)==list_ind(<a>; nil; u,v,w.v)
Given these definitions, it is straightforward to prove in Nuprl that hd satisfies
    >> All A:U1. All L:A list. hd(L) in A => ~(L=nil in A list)
    >> All A:U1. All x:A. All L:A list. hd(x.L)=x in A

Once the two goals above are proved they can be used in other proofs as lemmas. Similar facts for tl are also easy to prove.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995