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

*To*: pvs@csl.sri.com*Subject*: Boolean predicate to function*From*: Andre Renaud <ajr74@student.canterbury.ac.nz>*Date*: Mon, 05 Mar 2001 14:51:45 +1300*Sender*: pvs-owner@csl.sri.com

I have a fairly simple PVS question. In my current encoding I have a lot of functions defined in the form: foo(a, b : nat) : bool = ... These are generally a predicate which returns true if b is correct for some a. I have recently found the need to have these written in the following style as well: foo(a : nat): nat = ... where I now return the value of b. Is there a simple way to write the second function given the first? I've tried the following, but it isn't particularly successful: foo_return(a : nat): nat = FORALL(b : nat): if (foo(a, b)) then b else 0 endif But I get the following error message: Error: the assertion (COMPATIBLE? (TYPE LHS) (TYPE RHS)) failed Thanks, -- Andre Renaud Computer Science Department, University of Canterbury

**Follow-Ups**:**Re: Boolean predicate to function***From:*Dave Stringer-Calvert <dave_sc@csl.sri.com>

- Prev by Date:
**Re: Instantiation hints** - Next by Date:
**Re: Boolean predicate to function** - Prev by thread:
**Instantiations** - Next by thread:
**Re: Boolean predicate to function** - Index(es):