Selected Objects

def	mt	mt(l) == Case of l; nil  True ; a.as'  False
THM	mt_append	l,ll:'a List. mt(l @ ll)  mt(l) & mt(ll)
def	head	head(l) == hd(l)
THM	assert_of_null_is_mt	l:'a List. null(l)  mt(l)
def	rep_list	rep_list('a;l) == <n:. if n<||l|| then l[n] else arb('a) fi ,||l||>
THM	mt_def	mt(nil) = True  Prop{1} & ('a:Type{i}, x:'a, l:'a List. mt(cons(x; l)) = False  Prop{1})
def	it_sum	it_sum(l) == if null(l) then 0 else head(l)+it_sum(tl(l)) fi   (recursive)
THM	it_sum_def	it_sum(nil) = 0 & (l: List. mt(l)  it_sum(l) = head(l)+it_sum(tl(l))) & (x:, l: List. it_sum(cons(x; l)) = x+it_sum(l))
def	flatten	flatten(l) == if null(l) then nil else head(l) @ flatten(tl(l)) fi   (recursive)
def	map2	map2(f;l1;l2) == if null(l1) == then nil == else if null(l2) == else then nil == else else cons((f(head(l1),head(l2))); map2(f;tl(l1);tl(l2))) == else fi  == fi  (recursive)
def	every	every(p;l) == if null(l) then true else (p(head(l)))every(p;tl(l)) fi  (recursive)
THM	decidable__mt	l:'a List. Dec(mt(l))
def	hlist	hlist('a) == 'a List
def	his_list_rep	is_list_rep == r:('a). f:'a == r:('a). n: == r:('a). (r = <m:. if m<n then f(m) else @x:'a. true fi ,n>)
def	hrep_list	rep_list == l:'a List. rep_list('a;l)
def	habs_list	abs_list == r:('a). @a:'a List. (r = rep_list('a;a))
def	hnil	nil == nil
def	hcons	cons == x:'a. l:'a List. cons(x; l)
def	hnull	null == l:'a List. null(l)
def	hhd	hd == l:'a List. if null(l) then arb('a) else head(l) fi
THM	hhd_nuprl	'a:S, l:'a List. mt(l)  hd(l) = head(l)
def	htl	tl == l:'a List. tl(l)
def	hit_sum	it_sum == l: List. it_sum(l)
def	happend	append == l1:'a List. l2:'a List. l1 @ l2
def	hflat	flat == l:('a List) List. flatten(l)
def	hlength	length == l:'a List. ||l||
def	hmap	map == f:'a'b. l:'a List. map(f;l)
def	hmap2	map2 == f:'a'b. l1:'a. l2:'b. map2(f;l1;l2)
def	hel	el == n:. l:'a List. if n=0 then hd(l) else el(n-1,tl(l)) fi   (recursive)
THM	hel_nuprl	'a:S, n:, l:'a List. n<||l||  el(n,l) = l[n]
def	hevery	every == p:'a. l:'a List. every(p;l)
THM	his_list_rep_wd	'a:S.  all (r:hprod((hnum  'a); hnum (r:hprod(). equal (r:hprod(). (is_list_rep(r) (r:hprod(). ,exists (r:hprod(). ,(f:hnum  'a. exists (r:hprod(). ,(f:hnum  'a. (n:hnum. equal (r:hprod(). ,(f:hnum  'a. (n:hnum. (r (r:hprod(). ,(f:hnum  'a. (n:hnum. ,pair (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. cond (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. (lt(m,n) (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. ,f(m) (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. ,select(x:'a. t))) (r:hprod(). ,(f:hnum  'a. (n:hnum. ,,n))))))
THM	list_iso	'a:S. iso_pair('a List;('a);is_list_rep;rep_list;abs_list)
THM	hlist_ty_def	'a:S.  exists (rep:hlist('a)  hprod((hnum  'a); hnum). type_definition(is_list_rep,rep))
THM	hlist_iso_def	'a:S.  and (all(a:hlist('a). equal(abs_list(rep_list(a)),a)) ,all ,(r:hprod((hnum  'a); hnum). equal ,(r:hprod((hnum  'a); hnum). (is_list_rep(r) ,(r:hprod((hnum  'a); hnum). ,equal(rep_list(abs_list(r)),r))))
THM	hnil_def	'a:S. equal(nil,abs_list(pair((n:hnum. select(e:'a. t)),0)))

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html