Stream: Beginner Questions

Topic: Searching functions

view this post on Zulip 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?

view this post on Zulip 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: Feb 27 2024 at 08:17 UTC