Nuprl Definition : Comm-state
Comm-state() == st:Id fp-> pi_prefix() List × (Id × (pi_prefix() List)) List × Id × 𝔹 × ℕ
Definitions occuring in Statement :
pi_prefix: pi_prefix(),
fpf: a:A fp-> B[a],
Id: Id,
list: T List,
nat: ℕ,
bool: 𝔹,
product: x:A × B[x]
FDL editor aliases :
Comm-state
Latex:
Comm-state() == st:Id fp-> pi\_prefix() List \mtimes{} (Id \mtimes{} (pi\_prefix() List)) List \mtimes{} Id \mtimes{} \mBbbB{} \mtimes{} \mBbbN{}
Date html generated:
2015_07_23-AM-11_58_06
Last ObjectModification:
2012_08_30-PM-01_48_33
Home
Index