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

*To*: pvs-help@csl.sri.com*Subject*: A problem about rule "inst"*From*: Hu Chengjun <hcj@iist.unu.edu>*Date*: Tue, 23 Dec 1997 10:43:09 +0800

Hi all, I am a new user of PVS. Recently I met a problem and did not know how to solve it, so I put it here, hope someone can help me. I was trying to prove the following goal: {-1} (FORALL (A: Form[dcTV]): |>(([] A) => A)) [-2] |>([] (Des_1 /\ Des_2 => Triple)) |------- [1] |>(Des_1 /\ Des_2 => Req) I wanted to use rule "inst" to instantiate "A" to "(Des_1 /\ Des_2 => Triple)", but Rule? (inst -1 "(Des_1 /\ Des_2 => Req)") first argument has the wrong type Found: NL_types[dcTV].Form Expected: NL_types[dcTV].Term Restoring the state. I don't know why PVS expects type "Term" here, since "A" is of type "Form". However, if I instantiate "A" to "Des_1" or "Des_2", that is OK! So, to get the result I want, I have to write the following line in the .pvs file: TempVar : VAR FORM = Des_1 /\ Des_2 => Triple ; and then use (then* (inst -1 "TempVar") (expand "TempVar")) But this is, of course very inconvenient. Can anyone give an alternative solution? My PVS version is "PVS Version 2.0 Alpha Plus (patch level 2.376)". I will soon update it to 2.1, but I do not think it is a bug of version 2.0. Thanks! -- hcj@iist.unu.edu

- Prev by Date:
**Re: pvs question/suggestion...** - Next by Date:
**Re: A problem about rule "inst"** - Prev by thread:
**Recursive declarations** - Next by thread:
**Re: A problem about rule "inst"** - Index(es):