# Re: IF-EXISTS

```Hi Mauro,

What you probably want here is the "epsilon" function (or one of the
variants "choose" or "the").  In this case, I would probably write
something like

LET found(k: nat): bool = L`list(k)`f=f1 ) AND k < 10
IN IF (EXISTS (k: nat) : found(k))
THEN epsilon ! (k: nat): found(k)
ELSE 0
ENDIF

This just returns some k, not necessarily the smallest such, though you
said it was assumed to be unique.  The other possibility is to write a
recursive function, something like

FIND_REC(L : list_t, f1: nat, k: nat) :nat =
IF k = L`max
ELSIF L`list(k)`f=f1 AND k < 10 THEN k
ELSE FIND_REC(L, f1, k+1)
ENDIF
MEASURE L`max - k

FIND(L : list_t, f1: nat): nat = FIND_REC(L, f1, 0)

Hope this helps,
Sam

> 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.

```

• References:
• IF-EXISTS