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: 2016_05_17-PM-03_29_45 Last ObjectModification: 2014_07_25-PM-01_58_15 Theory : messages Home Index