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
Oh... simple enough. Thanks Lukas (again)!
If needed, there is also the inverse
Last updated: Feb 27 2024 at 08:17 UTC