## Stream: general

### 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 intros works.

#### 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 intros _

Last updated: May 08 2021 at 04:14 UTC