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

IF-EXISTS




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.