[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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).