I would like to find the concatenation function for strings in HOL.
I could not find it with find_consts, is there a better vehicle for this search?
string is just a type synonym for list of characters, and the find_* do not work well with those. So to answer you question the normal list append (@
) works for strings as well
Last updated: Jan 05 2025 at 20:18 UTC