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