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

[PVS-Help] Set clarification



The definition of min (from the prelude) is as follows:

  min(m, n): {p: real | p <= m AND p <= n}
    = IF m > n THEN n ELSE m ENDIF

where m and n are real numbers. My confusion is with respect to the
return type: it appears to me that min returns a set of real
numbers. Am I reading this correctly? If so, how is it that when used,
PVS knows the return type is a single value? For example

  min_le : LEMMA min(a,b) <= c IFF (a <= c OR b <= c)

Thanks

jerome