Jan van Brügge (Jul 10 2022 at 09:12): Jan van Brügge (Jul 10 2022 at 09:12):Hi, I am trying to prove a goal with ML. At first it did not work at all due to 'pending sort hypothesis'. After reading about that I removed all unnecessary forall-bound variables and the goal is proven as expected.
However if I add a definition for part of the body of the goal using Local_Theory.define_internal and try to prove that, i get 'pending sort hypothesis' again, even though the goal has no foralls at all.
Does anyone know why this is happening?
Last updated: Apr 25 2024 at 20:15 UTC