FDL > PVS > Div : Collection


------------------------------------------------------------------------
 Defines "div" according to the Ada Reference Manual

  div                 -- Ada Reference Manual division theory
  div  alt             -- Ada div defined recursively
  rem                 -- Ada Reference Manual rem theory
  mod  div  lems        -- relates mod to rem

 This div truncates toward zero on a negative argument.

 NOTE.  More specialized versions of mod and div are available
        in the nat_funs library,  The nat_funs library defines
        them over the nats only.

 See "number_theory" library for a div that truncates away from zero on a 
 negative argument:

    div_nt              -- Number theory division theory
    div_nt_alt          -- Number theory div defined recursively
 

 AUTHOR
 ------
 
   Ricky W. Butler                      email: *.*.******@****.****.***
   Mail Stop 130                     fax: (804) 864-xxxx
   NASA Langley Research Center   phone: (804) 864-xxxx
   Hampton, Virginia 23681-0001


   Paul S. Miner                  email: *.*.*****@****.****.***
   1 South Wright St. / MS 130      fax: (804) 864-xxxx
   NASA Langley Research Center   phone: (804) 864-xxxx
   Hampton, Virginia 23681      
------------------------------------------------------------------------

div alt
rem
mod div lems
div
floor div props
floor div lems