[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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
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
-- Paul S. Miner | phone: (757) 864-6201
-- 1 South Wright St. / MS 130 | fax: (757) 864-4234
-- NASA Langley Research Center | mailto:firstname.lastname@example.org
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/