Nuprl Definition : div_floor
a ÷↓ n ==
  eval r = a rem n in
  if (n) < (0)  then if (r) < (1)  then a ÷ n  else ((a ÷ n) - 1)  else if (r) < (0)  then (a ÷ n) - 1  else (a ÷ n)
Definitions occuring in Statement : 
callbyvalue: callbyvalue, 
less: if (a) < (b)  then c  else d
, 
remainder: n rem m
, 
divide: n ÷ m
, 
subtract: n - m
, 
natural_number: $n
Definitions occuring in definition : 
callbyvalue: callbyvalue, 
remainder: n rem m
, 
less: if (a) < (b)  then c  else d
, 
subtract: n - m
, 
natural_number: $n
, 
divide: n ÷ m
FDL editor aliases : 
div_floor
Latex:
a  \mdiv{}\mdownarrow{}  n  ==
    eval  r  =  a  rem  n  in
    if  (n)  <  (0)
          then  if  (r)  <  (1)    then  a  \mdiv{}  n    else  ((a  \mdiv{}  n)  -  1)
          else  if  (r)  <  (0)    then  (a  \mdiv{}  n)  -  1    else  (a  \mdiv{}  n)
Date html generated:
2016_05_13-PM-03_37_35
Last ObjectModification:
2015_09_22-PM-05_45_08
Theory : arithmetic
Home
Index