Stream: Coq devs & plugin devs

Topic: Printing an evar


view this post on Zulip Maxime Dénès (Jun 15 2020 at 21:59):

What is the recommended way to print an evar from a high level component? Evar.print seems to be low-level (i.e. does it handle evar names, etc?). Maybe @Pierre-Marie Pédrot knows?

view this post on Zulip Maxime Dénès (Jun 15 2020 at 22:00):

(in fact it is a set of evars that I want to print)

view this post on Zulip Pierre-Marie Pédrot (Jun 15 2020 at 22:01):

I'd go for Printer.pr_existential_key I believe

view this post on Zulip Maxime Dénès (Jun 15 2020 at 22:04):

oh!

view this post on Zulip Maxime Dénès (Jun 15 2020 at 22:04):

but that seems to be just an alias for Termops.pr_existential_key, right?

view this post on Zulip Maxime Dénès (Jun 15 2020 at 22:05):

wow, there's Printer.pr_evar and Printer.pr_existential as well

view this post on Zulip Maxime Dénès (Jun 15 2020 at 22:05):

none of these being documented, of course

view this post on Zulip Maxime Dénès (Jun 15 2020 at 22:06):

Termops.pr_existential_key does seem to print the name, as I was looking for, thanks!


Last updated: Oct 16 2021 at 07:02 UTC