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

Re: K_conversion



Hi,

Bart Jacobs writes:
   Date: Thu, 25 May 2000 15:25:05 +0200
   Subject: K_conversion

   Therefore, I am interested to know if other PVS users share
   my (negative) experiences with K_conversions.

After the first problems with the K_conversion I adopted the way
I work with PVS. The new rule is simple, it just says:

       Whenever PVS inserts a K_conversion, something is wrong.

To be fair, there is one application, where the K_conversion is
quite usefule. Consider:

    Pred[T : Type] : Theory
    Begin
      P,Q : Var PRED[T]

      neg(P) : PRED[T] = not P

      conj(P,Q) : PRED[T] = P and Q

      impl(P,Q) : PRED[T] = Q or not P

    end Pred

But still I would very much like to have a command "typecheck
without K_conversion".

   I know that one can see if K_conversions are inserted by
   checking the messages after typechecking. But this requires

The main problem for me is, that I can never remember the PVS
commands, that show the messages. From

view-prelude-file and view-prelude-theory

I learn, that there are files and theories in PVS. From that I
would expect, that there are

view-file-messages and view-theory-messages

But oops, first I can't view the messages, PVS has to show them,
and second for messages and warnings we don't have files but
pvs-files. So I start to thing interchangably about files and
pvs-files and about viewing and showing. But then I hit

show-proof-file
show-proofs-pvs-file

and I am lost. It takes me always three trials to find the
right command. 

Bye,

Hendrik