Re: [PVS-Help] Simple (?) question on PVS - constants offunctions of other constants

["David A. Wheeler" <dwheeler@xxxxxxxxxxxx>]

Sam Owre:
> The problem is that you've given a type where an expression is expected.
> You could do something like
>   comp: TYPE = [Compiler: CIO, Source: SRC -> CIO]
>   cmp: comp
>   Stage1: CIO = cmp(T, sA)

D'OH!  You're absolutely right.  It was staring me in the face, but somehow I just couldn't see it.

Thanks, I really appreciate that!!

--- David A. Wheeler