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

Re: pb with datatype and instance of datatype



> i have thise datatype
> 
> 	name: TYPE+
> 	natural : type -> nat 
>
>   .... deleted


I'm afraid this is so far from valid PVS that I cannot tell what you
are trying to do.   For example:

> 	natural : type -> nat 

Do you mean to overload "natural" with an uninterpreted function (in
which case it would be "natural: [type -> nat]" except "type" is a
keyword, so you'd need to declare and use a different identifier) or
do you want to make "nat" a synonym for "natural" (in which case it
would be "natural: type = nat", except they're already defined like
that in the prelude).  Similarly for the other declarations.

If you describe in words what you are trying to do, people here may be
able to help you express it in PVS.  But first, I suggest you try some
very simple examples from the manuals and tutorials and get a bit more
experience with PVS before trying to write your own specifications
from scratch.

Regards,
John Rushby