You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
doesn't work - no proof obligations are created for the placeholders (lean reports "no goals to be solved"), but omitting the proofs reports "don't know how to synthesize placeholder for argument 'h'".
have := IH ?_ s' ?_
obtain ⟨k, ⟨f⟩⟩ := this
works as expected.
The text was updated successfully, but these errors were encountered:
Example from #4707:
obtain ⟨k, ⟨f⟩⟩ := IH ?_ s' ?_
doesn't work - no proof obligations are created for the placeholders (lean reports "no goals to be solved"), but omitting the proofs reports "don't know how to synthesize placeholder for argument 'h'".
works as expected.
The text was updated successfully, but these errors were encountered: