Qiyuan Xu (May 20 2022 at 01:23): Qiyuan Xu (May 20 2022 at 01:23):I know they are both strings but of different semantics, but, what the semantics exactly is? Thanks!
Manuel Eberl (May 20 2022 at 08:38):FYI while it is entirely possible that you will get answers to such ML questions here on Zulip, the best source for such explanations is always Makarius, and he does not read Zulip, so you might want to try the isabelle-users mailing list as well. (important: NOT isabelle-dev)
Manuel Eberl (May 20 2022 at 08:39):He doesn't always reply in a very timely manner though…
Manuel Eberl (May 20 2022 at 08:39):(since he's obviously very busy)
Manuel Eberl (May 20 2022 at 08:39):But not very many people other than him do lots of Isabelle/ML programming these days, especially not concerning such internal things like bstring and xstring
Manuel Eberl (May 20 2022 at 08:43):From skimming the source code it seems to me that bstring is for bindings, i.e. things like fully qualified theorem names, constant names, type class names etc.
Manuel Eberl (May 20 2022 at 08:44):xstring on the other hand looks more like that kind of string that the user will see in the end, where unnecessary information has been stripped
Manuel Eberl (May 20 2022 at 08:44):for instance, if you do something like
ML_val ‹Proof_Context.extern_const @{context} "HOL.True"›
you will see that you get the output True (which according to the type signature is an xstring). In the other direction,
ML_val ‹Proof_Context.intern_const @{context} "True"›
gives you HOL.True, which is a bstring.
Qiyuan Xu (May 22 2022 at 11:40):oh, these are really interesting! very thank you!
Last updated: Dec 21 2024 at 16:20 UTC