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

*To*: pvs@csl.sri.com*Subject*: Re: K_conversion*From*: Hendrik Tews <tews@tcs.inf.tu-dresden.de>*Date*: Fri, 26 May 2000 13:15:57 +0200 (MET DST)*Delivery-Date*: Fri May 26 04:16:04 2000*In-Reply-To*: <200005251325.PAA05880@pandora.cs.kun.nl>*References*: <200005251325.PAA05880@pandora.cs.kun.nl>

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

**References**:**K_conversion***From:*Bart Jacobs <Bart.Jacobs@cs.kun.nl>

- Prev by Date:
**Re: K_conversion** - Next by Date:
**Re: K_conversion** - Prev by thread:
**Re: K_conversion** - Next by thread:
**PhD STUDENTSHIP available** - Index(es):