Nuprl Definition : PiDataVal
PiDataVal() ==
Id + id:Id × Name + from:Id × (pi_prefix() List) + val:Name × ℕ + Unit + Unit + ℕ × Id × ℕ × Name + (rndv2:ℕ
× Id
× ℕ
× Name × ℕ)
Definitions occuring in Statement :
pi_prefix: pi_prefix(),
Id: Id,
name: Name,
list: T List,
nat: ℕ,
unit: Unit,
product: x:A × B[x],
union: left + right
FDL editor aliases :
PiDataVal
Latex:
PiDataVal() ==
Id + id:Id \mtimes{} Name + from:Id
\mtimes{} (pi\_prefix() List) + val:Name
\mtimes{} \mBbbN{} + Unit + Unit + \mBbbN{} \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} Name + (rndv2:\mBbbN{}
\mtimes{} Id
\mtimes{} \mBbbN{}
\mtimes{} Name \mtimes{} \mBbbN{})
Date html generated:
2015_07_23-AM-11_34_22
Last ObjectModification:
2012_08_30-PM-01_42_06
Home
Index