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: Apr 27 2024 at 12:25 UTC