Nuprl Definition : bound-domain

bound-domain(f;n;e) ==  λx.if (x) < (0)  then ⊥  else if (x) < (n)  then f x  else (exception(e; x))


Definitions occuring in Statement :  bottom: ⊥,  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  natural_number: $n
Definitions occuring in definition :  lambda: λx.A[x],  natural_number: $n,  bottom: ⊥,  less: if (a) < (b)  then c  else d,  apply: f a
FDL editor aliases :  bound-domain
Latex:
bound-domain(f;n;e)  ==    \mlambda{}x.if  (x)  <  (0)    then  \mbot{}    else  if  (x)  <  (n)    then  f  x    else  (exception(e;  x))


Date html generated: 2019_06_20-PM-02_50_03
Last ObjectModification: 2019_02_08-PM-03_11_39

Theory : continuity


Home Index