WhoCites
Definitions
GenAutomata
Sections
NuprlLIB
Doc
Who Cites reject?
reject
Def as\[i] == if i
0
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
i
j ==
j <
i
Thm*
i,j:
. (i
j)
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:
WhoCites
Definitions
GenAutomata
Sections
NuprlLIB
Doc