Hernán Rajchert (Oct 05 2022 at 14:00): Hernán Rajchert (Oct 05 2022 at 14:00):Hi there! I'm new to isabelle, and I'm doing some work that requires to export some code to haskell. I noticed that plain string are exported as Char b0 b1 ..., and that there is a String.literal that exports to Haskell [Char]. I've seen we have implode and explode to convert from one to the other, but is there a way for me to define a code_unfold or similar so that every instance of string is replaced by String.literal?
Last updated: Apr 19 2024 at 16:20 UTC