[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: [PVS-Help] Min value in a set
It distinguishes between them on the basis of the number of
arguments. Since both are in prelude, no IMPORTING statements are
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
The NASA libraries provide min and max over sets over a bounded domain.
for information about how to install these.
> -----Original Message-----
> From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx
> 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).