[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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
I tried something like this:
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
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....