Nuprl Definition : bigger-int
bigger-int(n;L) ==
  accumulate (with value x and list item y):
   eval x = x in
   eval y = y in
     if x ≤z y then y + 1 else x fi 
  over list:
    L
  with starting value:
   n)
Definitions occuring in Statement : 
list_accum: list_accum, 
le_int: i ≤z j
, 
callbyvalue: callbyvalue, 
ifthenelse: if b then t else f fi 
, 
add: n + m
, 
natural_number: $n
Definitions occuring in definition : 
list_accum: list_accum, 
callbyvalue: callbyvalue, 
ifthenelse: if b then t else f fi 
, 
le_int: i ≤z j
, 
add: n + m
, 
natural_number: $n
FDL editor aliases : 
bigger-int
Latex:
bigger-int(n;L)  ==
    accumulate  (with  value  x  and  list  item  y):
      eval  x  =  x  in
      eval  y  =  y  in
          if  x  \mleq{}z  y  then  y  +  1  else  x  fi 
    over  list:
        L
    with  starting  value:
      n)
Date html generated:
2016_05_14-PM-01_55_20
Last ObjectModification:
2015_09_22-PM-05_55_07
Theory : list_1
Home
Index