Hanno Becker (Mar 15 2023 at 08:33): 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?
Lukas Stevens (Mar 17 2023 at 21:10):You can turn a HOL equality into a Pure equality using the theorem eq_reflection.
Hanno Becker (Mar 18 2023 at 06:36):Oh... simple enough. Thanks Lukas (again)!
Jan van Brügge (Mar 20 2023 at 10:15):If needed, there is also the inverse meta_eq_to_obj_eq
Last updated: Dec 21 2024 at 16:20 UTC