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

Re: Subtyping




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


The construction that Paul gives is part of PVS 2.2, but will be removed
from the language in the next release.  It is a hangover from EHDM, and
serves no useful purpose in PVS (which is why it does not appear in the
language manual, other than in the grammar fragments) as you can get the
desired effect by using a coercion:

       lambda (x : P) : E:Q

Note also that in PVS 2.3, the syntax for coercions will change from
"expr : type-expr" to "expr :: type-expr" to reduce the ambiguity in
the grammar.

Dave

---
Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com