Nuprl Definition : ws_single_compseq_tag_def
11,40
postcript
pdf
ws_single{
ws
single
compseq
tag
def
:ObjectId}
ws_single
(
F
;
p
)
== compseq(weighted-sum([
p
];
F
); (0 + ((
F
(0)) *
p
)))
latex
clarification:
ws_single{
ws
single
compseq
tag
def
:ObjectId}
ws_single
(
F
;
p
)
== compseq(weighted-sum([
p
/ []];
F
); (0 + ((
F
(0)) *
p
)))
latex
Definitions
weighted-sum(
p
;
F
)
,
[
car
/
cdr
]
,
[]
,
r
+
s
,
r
*
s
,
f
(
a
)
,
#$n
origin