RE: [PVS-Help] Min value in a set

["Butler, Ricky W. (LARC-D320)" <r.w.butler@xxxxxxxx>]

Jerome,
   It distinguishes between them on the basis of the number of
arguments.  Since both are in prelude, no IMPORTING statements are
needed.

Note. See theory "finite_sets_minmax" in the "finite_sets" library for 
a more general min/max over sets.
      This can be located in the lib subdirectory of your installation
directory.  It is imported as follows

       IMPORTING finite_sets@finite_sets_minmax

The NASA libraries provide min and max over sets over a bounded domain.

       IMPORTING reals@bounded_reals

See http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
for information about how to install these.

Rick

> -----Original Message-----
> From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx
[mailto:pvs-
> help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx] On Behalf Of Jerome
> Sent: Tuesday, March 11, 2008 8:03 PM
> To: pvs-help@xxxxxxxxxxx
> Subject: [PVS-Help] Min value in a set
> 
> I would like to use both 'min' operations in the prelude: min over a
> set and min of two values - how do I do it? In the former, I think the
> min found in 'min_nat' would do the trick, but I'm not sure how to
> access it. PVS always seems to think I want the min within 'real_defs'
> (which I do, for the latter).
> 
> jerome