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

Re: [PVS-Help] Elementary Question


It looks like you're mixing up the syntax for definitions with that for
types.  I expect what you want is

  count_eq_zero(i): bool = (if i=0 then true else false endif)

which is equivalent to

  count_eq_zero: [nat->bool] = lambda i: (if i=0 then true else false endif)


Shi Hui Woon <shihuiwoon@yahoo.com.sg> wrote:

> Hi, I've got a quick question. I've got a function, count_eq_zero defined below
> but when I put it to typecheck, it shows: Found '!id!' when expecting ')'. How
> should I define the function then?
> [sum_verify: THEORY
>    BEGIN
>    n,i: VAR nat
>    count_eq_zero(i): TYPE = [nat->bool] = (if i=0 then true else false endif)
> ...]
> Thanks
> -------------------------------------------------------------------------------
> New Email addresses available on Yahoo!
> Get the Email name you've always wanted on the new @ymail and @rocketmail.
> Hurry before someone else does!