WhoCites Definitions GenAutomata Sections NuprlLIB Doc

Who Cites reject?
rejectDef as\[i] == if i0 tl(as) else Case of as; nil nil ; a'.as' [a' / as'\[i-1]] fi (recursive)
Thm* A:Type, l:A List, n:. l\[n] A List
tl Def tl(l) == Case of l; nil nil ; h.t t
Thm* A:Type, l:A List. tl(l) A List
le_int Def ij == j < i
Thm* i,j:. (ij)
lt_int Def i < j == if i < j true ; false fi
Thm* i,j:. (i < j)
bnot Def b == if b false else true fi
Thm* b:. b

Syntax:as\[i] has structure: reject(i; as)

About:
listconsnillist_indbool
bfalsebtrueifthenelseintnatural_numbersubtract
lessrecursive_def_noticeuniversememberall
!abstraction

WhoCites Definitions GenAutomata Sections NuprlLIB Doc