Stream: Coq users

Topic: Computation Variant of In and String Comparison

Julia Dijkstra (Jan 08 2024 at 23:11):

I was wondering if there is a variant of in that returns a boolean if a given item is in a list, because I could not find it. I also wonder how one should do string comparison - right now I resorted to writing this to indicate whether a string is in a list of strings, but it is quite bothersome to work with.

Fixpoint sym_in (sym: string) (l: list string): bool :=
    match l with
    | [] => false
    | head :: tail =>
        if string_dec head sym then true
        else sym_in sym tail
    end.

Julia Dijkstra (Jan 09 2024 at 00:06):

I found existsb and eqb. Not sure why existsb is so named so much differently from In however.

Meven Lennon-Bertrand (Jan 09 2024 at 09:37):

existsb is more general, it finds elements satisfying a predicate which can be anything decidable, not just the equality with a given thing

Meven Lennon-Bertrand (Jan 09 2024 at 09:39):

On the logical side, one can express existence in the list using only In, as existsb_exists shows. But on the boolean side, existsb is more flexible

Last updated: Sep 15 2024 at 13:02 UTC