WhoCites
Definitions
mb
event
system
7
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites update?
update
Def
f
[
x
:=
v
](
y
) == if
eq
(
y
,
x
)
v
else
f
(
y
) fi
Thm*
A
,
B
:Type,
eq
:(
A
A
),
f
:(
A
B
),
x
:
A
,
v
:
B
.
f
[
x
:=
v
]
A
B
Syntax:
f
[
x
:=
v
]
has structure:
update(
eq
;
f
;
x
;
v
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
mb
event
system
7
Sections
EventSystems
Doc
v else f(y) fi
A,B:Type, eq:(A
A
), f:(AB), x:A, v:B. f[x:=v] 
AB v else f(y) fiA,B:Type, eq:(AA), f:(AB), x:A, v:B. f[x:=v] AB
