Re: [PVS-Help] Elementary Question

[Sam Owre <owre@xxxxxxxxxxx>]

Hi,

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)

Regards,
Sam  

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!