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?
You can turn a HOL equality into a Pure equality using the theorem eq_reflection
.
Oh... simple enough. Thanks Lukas (again)!
If needed, there is also the inverse meta_eq_to_obj_eq
Last updated: Dec 07 2024 at 16:22 UTC