Nuprl Definition : coW2natinf
coW2natinf(w;n) == if (fst(w) =z 1) then if (n =z 0) then tt else coW2natinf(coW-item(w;⋅);n - 1) fi else ff fi
Definitions occuring in Statement :
coW-item: coW-item(w;b),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
bfalse: ff,
btrue: tt,
it: ⋅,
pi1: fst(t),
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
bfalse: ff,
natural_number: $n,
subtract: n - m,
it: ⋅,
coW-item: coW-item(w;b),
btrue: tt,
eq_int: (i =z j),
ifthenelse: if b then t else f fi ,
pi1: fst(t)
FDL editor aliases :
coW2natinf
Latex:
coW2natinf(w;n) ==
if (fst(w) =\msubz{} 1) then if (n =\msubz{} 0) then tt else coW2natinf(coW-item(w;\mcdot{});n - 1) fi else ff fi
Date html generated:
2018_07_29-AM-09_29_13
Last ObjectModification:
2018_07_27-PM-03_22_10
Theory : basic
Home
Index