Nuprl Definition : power-type
(T^k) == fix((λpower-type,k. if (k =z 0) then Unit else T × (power-type (k - 1)) fi )) k
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
unit: Unit,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
product: x:A × B[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
unit: Unit,
product: x:A × B[x],
apply: f a,
subtract: n - m,
natural_number: $n
FDL editor aliases :
power-type
Latex:
(T\^{}k) == fix((\mlambda{}power-type,k. if (k =\msubz{} 0) then Unit else T \mtimes{} (power-type (k - 1)) fi )) k
Date html generated:
2016_05_15-PM-06_05_36
Last ObjectModification:
2015_09_23-AM-08_01_15
Theory : general
Home
Index