Nuprl Definition : pax-p2a-type
pax-p2a-type(es;accpts) == type-of-message(es;pax_p2a();accpts;Id 
PValue())
Proof not projected
Definitions occuring in Statement :
pax_p2a: pax_p2a(),
PValue: PValue(),
type-of-message: type-of-message(es;nm;locs;T),
Id: Id,
product: x:A B[x]
Definitions :
type-of-message: type-of-message(es;nm;locs;T),
pax_p2a: pax_p2a(),
product: x:A B[x],
Id: Id,
PValue: PValue()
FDL editor aliases :
pax-p2a-type
pax-p2a-type(es;accpts) == type-of-message(es;pax\_p2a();accpts;Id \mtimes{} PValue())
Date html generated:
2011_10_20-PM-11_50_38
Last ObjectModification:
2011_05_24-PM-01_21_28
Home
Index