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: Dec 07 2023 at 16:21 UTC