Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
No other cites to report in NuprlPrimitives
let
Def let
x
=
a
in
b
(
x
) == (
x
.
b
(
x
))(
a
)
Thm*
A
,
B
:Type,
a
:
A
,
b
:(
A
B
). let
x
=
a
in
b
(
x
)
B
Syntax:
let
x
=
a
in
b
(
x
)
has structure:
let(
a
;
x
.
b
(
x
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
x.b(x))(a)
A,B:Type, a:A, b:(A
B). let x = a in b(x) 
Bx.b(x))(a)A,B:Type, a:A, b:(AB). let x = a in b(x) B
