Email Gateway (Aug 22 2022 at 11:04): Email Gateway (Aug 22 2022 at 11:04):From: Lars Hupel <hupel@in.tum.de>
Dear Rene and Christian,
using your AFP entry, I was trying to produce a "show" instance for a
large-ish datatype containing a string, and it failed. I managed to find a
small reproducing test case (see attached). The error message reads:
no show-function available for type "String.char"
... which I find confusing since you do instantiate "show" for characters.
What am I doing wrong?
Cheers
Lars
Scratch.thy
Email Gateway (Aug 22 2022 at 11:05):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Lars,
thanks for the report, you have actually detected an omission in our setup. Whereas we registered „char“ in the class show, we did not register it in the generator. E.g., in Show_Instances you see the lines
#> Show_Generator.register_foreign_showsp @{typ unit} @{term "showsp_unit"} @{thm show_law_unit}
#> Show_Generator.register_foreign_showsp @{typ bool} @{term "showsp_bool"} @{thm show_law_bool}
#> Show_Generator.register_foreign_showsp @{typ nat} @{term "showsp_nat"} @{thm show_law_nat}
#> Show_Generator.register_foreign_showsp @{typ int} @{term "showsp_int"} @{thm show_law_int}
#> Show_Generator.register_foreign_showsp @{typ rat} @{term "showsp_rat"} @{thm show_law_rat}
but no line for „char“.
We are working on the fix which should be finished soonish, by providing the required @{thm show_law_char}.
Cheers,
Christian and René
Email Gateway (Aug 22 2022 at 11:05):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Lars,
here is a fix:
insert into the file Show_Instances.thy the following lines:
abbreviation showsp_char :: "char showsp"
where
"showsp_char == shows_prec"
lemma show_law_char [show_law_intros]:
"show_law showsp_char x"
by (rule show_lawI) (simp add: show_law_simps)
and the line
#> Show_Generator.register_foreign_showsp @{typ char} @{term "showsp_char"} @{thm show_law_char}
somewhere in the lines mentioned before. Just let us know, if there are further problems,
Cheers,
René
Last updated: Apr 26 2024 at 12:28 UTC