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

Re: [PVS-Help] Cotuple mutually exclusive component types


   I have been working with cotuples.  I'm hitting a problem I don't know
   how to solve.  The problem boils down to proving the following lemma:
Cotuples do not work yet in PVS. See my bug reports #779, #782,
and #783. Sam Owre provided patches for the typechecking
problems, but the prover, especially the decision procedures do
not seem to support cotuples yet.

You have to use datatypes for the time being.