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

*To*: pvs-help@csl.sri.com*Subject*: IF-EXISTS*From*: Mauro Gargano <mauro@troubadix.cs.uni-sb.de>*Date*: Tue, 3 Dec 2002 18:05:42 +0100 (CET)*Sender*: pvs-help-owner@csl.sri.com

Hallo to everybody, I have the need to create a function to that return the index of a element (for which a predicate holds) of a list (assumed that this element is unique). I tried something like this: help : THEORY BEGIN A : TYPE+ = [# f: nat, g: nat, h:nat #] list_t: TYPE = [# max:nat, list: [below(max) -> A] #] % I just want to define a find function .... FIND(L : list_t, f1: nat) :nat = ( IF (( EXISTS (k: nat) : L`list(k)`f=f1 ) AND k < 10) THEN k ELSE 0 ENDIF ) END help but whithout success. Has someone an idea of how to do this? and, in the case I reject the uniqueness-hypotesis, what happens? Obviously I should get in return a sublist, but how.... Thanks, Mauro Gargano.

- Prev by Date:
**Re: Error: attempt to call `PARSE-FILE'** - Next by Date:
**Re: IF-EXISTS** - Prev by thread:
**About an error** - Next by thread:
**Re: IF-EXISTS** - Index(es):