Stream: Isabelle/ML

Topic: HOL Conversions


view this post on Zulip Hanno Becker (Mar 15 2023 at 08:33):

Hi. From what I've seen, the conversion mechanism seems to operate on the level of Pure. Is there an extension supporting conversions derived from HOL equalities?

view this post on Zulip Lukas Stevens (Mar 17 2023 at 21:10):

You can turn a HOL equality into a Pure equality using the theorem eq_reflection.

view this post on Zulip Hanno Becker (Mar 18 2023 at 06:36):

Oh... simple enough. Thanks Lukas (again)!

view this post on Zulip Jan van Brügge (Mar 20 2023 at 10:15):

If needed, there is also the inverse meta_eq_to_obj_eq


Last updated: Feb 27 2024 at 08:17 UTC