[PVS-Help] Simple (?) question on PVS - constants of functions ofother constants

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

Hi - I'm a new PVS user, and I'm trying to translate a hand-created proof into PVS.  But almost immediately I'm running into trouble; I can't seem to define constants that are the results of functions on other constants.  Instead I get "No resolution for comp with arguments of possible types..." error messages.

What's wrong in the tiny snippet below?  I presume it's really obvious, but I don't know what it is.

I'm basically trying to prove some assertions related to compiling code.  I do NOT want to define the specific compilation function. Instead, I need to make general assertions like "if a function that compiles something meets properties <P>, then claims <C> will be true."

Thanks.

--- David A. Wheeler

================================================

problem: THEORY
 BEGIN
  SRC: TYPE % Any Source code has this type
  CIO: TYPE % Any input/output of a compilation other than SRC

  % A compilation step is a function that accepts a CIO (the compiler)
  % and SRC (the source code), and produces a CIO (the compiled result)
  comp: TYPE = [Compiler: CIO, Source: SRC -> CIO]

  sA: SRC
  T: CIO  % T is a compiler

  Stage1: CIO = comp(T, sA)
  % This will produce this error message:
  % Expecting an expression
  % No resolution for comp with arguments of possible types: 
  %  T : CIO
  %  sA : SRC

  % This doesn't work either:
  Stage1: CIO
  Stage1_is: AXIOM Stage1 = comp(T, sA)
  % This will produce this error message:
  % Expecting an expression
  % No resolution for comp with arguments of possible types: 
  %  T : CIO
  %  sA : SRC

END problem