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

typecheck error

Dear PVS helpers,

I am a new PVS user, and am trying to augment the theory for finite 
sequences. I have the following code:

  finseq_props [T: TYPE] : THEORY
    a, b: VAR finseq[T]
    dummy: finseq[T]
    o_empty0: THEOREM b = empty_seq IMPLIES a o b = a
    o_empty1: THEOREM a o empty_seq = a
    o_empty2: THEOREM empty_seq o a = a
    o_dummy1: THEOREM a o dummy = a
    o_dummy2: THEOREM dummy o a = a
  END finseq_props

When I typecheck this, I get an error for o_empty2 which reads: "could 
not determine the full theory instance for =". The other theorems 
typecheck fine. Does anyone know what is causing this problem?

Thank you,
Gregory Kulczycki

  Gregory W. Kulczycki             West Virginia University
  gregwk@cs.wvu.edu                Reusable Software Research Group
  http://www.cs.wvu.edu/~gregwk    http://www.cs.wvu.edu/~resolve