\/(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?