Stream: Isabelle/ML

Topic: Pending sort hypothesis with definition

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: Dec 21 2024 at 16:20 UTC