Topic: intros unfolding
Patrick Massot (Jun 27 2018 at 16:13):
Is this normal?
example (P Q : Prop) : P → Q := begin intros, -- context has a: P, goal is now Q sorry end def f (P Q : Prop) := P → Q example (P Q : Prop) : f P Q := begin intros, -- nothing happen :-( intros a, -- context is a : P, goal is now Q sorry end
It seems this prevents
finish to work successfully in some cases without a preliminary
intros a b c d e f
Kevin Buzzard (Jun 27 2018 at 16:25):
that's kind of interesting. If you make f reducible, or unfold it explicitly, maybe
Patrick Massot (Jun 27 2018 at 16:35):
Of course explicit unfolding works. But reducible is not enough.
Simon Hudon (Jun 27 2018 at 16:36):
you can also try
Last updated: Aug 03 2023 at 10:10 UTC