[PVS-Help] a problem

[applehopedream <applehopedream@xxxxxxx>]

 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?