Zulip Chat Archive

Stream: general

Topic: intros unfolding

Patrick Massot (Jun 27 2018 at 16:13):

Is this normal?

example (P Q : Prop)  : P  Q :=
intros, -- context has a: P, goal is now Q

def f (P Q : Prop) := P  Q

example (P Q : Prop)  : f P Q :=
intros, -- nothing happen :-(
intros a, -- context is a : P, goal is now Q

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: Dec 20 2023 at 11:08 UTC