isMember {A} (testEq : A → A → Bool) (element : A) (list : List A) : Bool := case list of {
| nil := false
| x :: xs := testEq element x || isMember testEq element xs
};
Moreover, we'd like to support simultaneously casing on multiple elements with the help of the Pair type (or any other product type) and still detect termination.
zipWith {A B C} (f : A -> B -> C) (list1 : List A) (list2 : List B) : List C := case list1, list2 of {
| nil, _ := nil
| _, nil := nil
| x :: xs, y :: ys := f x y :: zipWith f xs ys
};
E.g. it should be possible to write
Moreover, we'd like to support simultaneously casing on multiple elements with the help of the
Pair
type (or any other product type) and still detect termination.