Nuprl Definition : basicMessage
A basic message is a header and a value whose type depends on the header.⋅
basicMessage(f) ==  h:Name × (f h)
Definitions occuring in Statement : 
name: Name
, 
apply: f a
, 
product: x:A × B[x]
FDL editor aliases : 
basicMessage
Latex:
basicMessage(f)  ==    h:Name  \mtimes{}  (f  h)
Date html generated:
2015_07_21-PM-04_48_08
Last ObjectModification:
2014_07_25-PM-01_58_15
Home
Index