Zulip Chat Archive

Stream: lean4

Topic: refine tactic syntax for inductive types


view this post on Zulip Yakov Pechersky (Mar 24 2021 at 05:44):

What's the right incantation to make the following work?

example (hp : p) (hq : q) : And p q := by
  refine _, _; -- errors here, does not produce two goals
  exact hp; -- says "no goals to be solved" here
  exact hq

view this post on Zulip Mario Carneiro (Mar 24 2021 at 05:45):

example (hp : p) (hq : q) : And p q := by
  refine ?_, ?_;
  exact hp;
  exact hq

view this post on Zulip Yakov Pechersky (Mar 24 2021 at 05:46):

Thanks Mario. I see that produces two cases refine_1 and refine_2. Is there a way to name them?

view this post on Zulip Mario Carneiro (Mar 24 2021 at 05:47):

example (hp : p) (hq : q) : And p q := by
  refine ?a, ?b
  case a => exact hp
  case b => exact hq

view this post on Zulip Yakov Pechersky (Mar 24 2021 at 05:47):

Sweet, thanks

view this post on Zulip Yakov Pechersky (Mar 24 2021 at 05:48):

By the way, when did we get Go-To-Defn working in VSCode?! It's awesome!

view this post on Zulip Yakov Pechersky (Mar 24 2021 at 05:48):

And the infoview working...


Last updated: May 18 2021 at 23:14 UTC