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

TLAPS and string search algorithms

As a fun side-project with TLAPS, I'd like to prove correctness of some string search algorithms. However, TLAPS says it doesn't support quantification over tuples and set constructors. Would this affect ability to prove things about strings (which I guess are represented by sequences of characters)?