intros unfolding

Stream: general

[Patrick Massot]

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]

that's kind of interesting. If you make f reducible, or unfold it explicitly, maybe intros works.

[Patrick Massot]

Of course explicit unfolding works. But reducible is not enough.

[Simon Hudon]

you can also try intros _