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

Re: [PVS-Help] a problem


It's not very well documented, but when you input these in the prover,
the '\' symbol is treated as an escape.  It must be doubled to be
properly accepted, for example, (expand "\\/").  

There are precedences for all the operators, these are described in
section 5.1 of the PVS Language Reference Manual.  These precedence
rules are syntactic, so redeclaring them will not change the

Sam Owre

applehopedream <applehopedream@xxxxxxx> wrote:

> Date: Mon, 28 Jul 2008 22:55:28 +0800 (CST)
> From: applehopedream <applehopedream@xxxxxxx>
> To: pvs <pvs-help@xxxxxxxxxxx>
> Subject: [PVS-Help] a problem
>  Hi,
>    In my study of PVS,I come across some problems,I hope someone can help me
> .Thank you!
>    When I redeclare the PVS definable symbols,\/  I declare them as follows: 
>          \/(f1,f2)          : form = ftwo(f1,f2,tor);
>   form is an abstract datatype which is my defined before.and when I use these
> two symbols in the proving ,the prover report errors:
>   first argument to / has the wrong type
>   Found : fomr_adt.form
>   Expected : number_fields.numfield
>  But I redeclare other definable symbols like =>,is right and => is defined as
> follows:
>  =>(f1,f2)           : form = ftwo(f1,f2,timpl);
> I don't know why ?
> by the way, in the reserved words ,special symbols and definable symbols ,are
> there some precedence rules?for example,NOT,AND,OR are they have the same
> precedence in the use?