[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] nonempty type tcc
This is a bug, I added it to our bugs list.
You can work around it by using the lemma "PROC_nonempty" that is
generated in the proc theory (M-x prettyprint-expanded shows this).
robert <firstname.lastname@example.org> wrote:
> I've just changed to version 3.2 and a problem has cropped up.
> I have a theory
> proc: THEORY
> PROC: TYPE+
> end proc
> I import this theory via library, eg,
> sq_abstract: THEORY
> lib: LIBRARY = "whatever"
> importing lib@proc
> pp: PROC
> end sq_abstract
> The type checker generates the tcc
> % Existence TCC generated (at line 97, column 1) for pp: PROC
> % unfinished
> pp_TCC1: OBLIGATION EXISTS (x: PROC): TRUE;
> This isn't proved when I use M-x prove-tccs-theory (ie, using (tcc)
> or (grind)).
> I introduced a theorem identical to pp_TCC1 in theory proc and was able
> to prove it straight away using (grind).
> How can I prove the tcc obligation?