Zulip Chat Archive

Stream: general

Topic: intros unfolding


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 27 2018 at 16:35):

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

view this post on Zulip Simon Hudon (Jun 27 2018 at 16:36):

you can also try intros _


Last updated: May 08 2021 at 04:14 UTC