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

Subtyping



Michel Levy writes:
 > I try to express in PVS that the unnamed function (Lambda (x:P) :
 > expression) has a result of type Q.
 > I don't find a solution (without giving a name) through the reference's
 > manual.

Try (lambda (x:P)->Q: expression)

This will generate a TCC to show that expression has type Q.

This is in the syntax given on p. 38 of the language referece manual.

I am not aware of an example of this in the manual, but it is part of
the language.  

-- 
-- Paul S. Miner                | phone: (757) 864-6201
-- 1 South Wright St. / MS 130  | fax:   (757) 864-4234
-- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/