[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