Definitions
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
le
Def
A
B
==
B
<
A
Thm*
i
,
j
:
. (
i
j
)
Prop
tl
Def
tl(
l
) == Case of
l
; nil
nil ;
h
.
t
t
Thm*
A
:Type,
l
:
A
List. tl(
l
)
A
List
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
list
1
Sections
StandardLIB
Doc
B == 
B<A
i,j:
. (ij) 
Prop
nil ; h.t tA:Type, l:A List. tl(l) A ListB == B<Ai,j:. (ij) Prop nil ; h.t tA:Type, l:A List. tl(l) A List
