hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* 'a:S. equal(nil,abs_list(pair((n:hnum. select(e:'a. t)),0)))[hnil_def]
Thm* 'a:S. 
Thm* and
Thm* (all(a:hlist('a). equal(abs_list(rep_list(a)),a))
Thm* ,all
Thm* ,(r:hprod((hnum  'a); hnum). equal
Thm* ,(r:hprod((hnum  'a); hnum). (is_list_rep(r)
Thm* ,(r:hprod((hnum  'a); hnum). ,equal(rep_list(abs_list(r)),r))))		[hlist_iso_def]
Thm* 'a:S. 
Thm* exists
Thm* (rep:hlist('a)  hprod((hnum  'a); hnum). type_definition
Thm* (rep:hlist('a)  hprod((hnum  'a); hnum). (is_list_rep
Thm* (rep:hlist('a)  hprod((hnum  'a); hnum). ,rep))		[hlist_ty_def]
Thm* 'a:S. iso_pair('a List;('a);is_list_rep;rep_list;abs_list)[list_iso]
Thm* 'a:S. 
Thm* all
Thm* (r:hprod((hnum  'a); hnum
Thm* (r:hprod(). equal
Thm* (r:hprod(). (is_list_rep(r)
Thm* (r:hprod(). ,exists
Thm* (r:hprod(). ,(f:hnum  'a. exists
Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. equal
Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. (r
Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,pair
Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. cond
Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. (lt(m,n)
Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. ,f(m)
Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. ,select(x:'a. t)))
Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,,n))))))		[his_list_rep_wd]
Thm* 'a:S. hlist('a)  S[hlist_wf]
Thm* 'a:S. el  (hnum  hlist('a)  'a)[hel_wf]
Thm* 'a:S. hd  (hlist('a)  'a)[hhd_wf]
Thm* 'a:S, n:, l:'a List. n<||l||  el(n,l) = l[n][hel_nuprl]
Thm* 'a:S, l:'a List. mt(l)  hd(l) = head(l)[hhd_nuprl]
Thm* l:'a List. Dec(mt(l))[decidable__mt]
Thm* 'a:S. 'a List  S[list_wf_stype]
Thm* 'a:Type, p:('a), l:'a List. every(p;l)  [every_wf]
Thm* 'a,'b,'c:Type, f:('a'b'c), l1:'a List, l2:'b List.
Thm* map2(f;l1;l2)  'c List		[map2_wf]
Thm* 'a:Type, l:('a List) List. flatten(l)  'a List[flatten_wf]
Thm* it_sum(nil) = 0
Thm* & (l: List. mt(l)  it_sum(l) = head(l)+it_sum(tl(l)))
Thm* & (x:, l: List. it_sum(cons(x; l)) = x+it_sum(l))		[it_sum_def]
Thm* l: List. it_sum(l)  [it_sum_wf]
Thm* 'a:S, l:'a List. rep_list('a;l)  ('a)[rep_list_wf]
Thm* mt(nil) = True  Prop{1}
Thm* & ('a:Type{i}, x:'a, l:'a List. mt(cons(x; l)) = False  Prop{1})		[mt_def]
Thm* 'a:Type, l:'a List. ||l||  [length_wf_nat]
Thm* l:'a List. null(l)  mt(l)[assert_of_null_is_mt]
Thm* 'a:Type, l:'a List. mt(l)  head(l)  'a[head_wf]
Thm* l,ll:'a List. mt(l @ ll)  mt(l) & mt(ll)[mt_append]
Thm* 'a:Type{i}, l:'a List. mt(l)  Prop{1}[mt_wf]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 hol hol min hol bool hol restr binder hol num hol pair hol prim rec hol arithmetic 1

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

hol list 1 Sections HOLlib Doc