Gergely Buday (Jun 14 2023 at 14:08): Gergely Buday (Jun 14 2023 at 14:08):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?
Jan van Brügge (Jun 14 2023 at 15:19):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: Nov 13 2025 at 04:27 UTC