Order of goals after `apply`

Stream: general

[David Loeffler]

Here's a Lean tactic behaviour that I'm not very keen on:

def P : Prop := sorry
def Q : Prop := sorry
def R : Prop := sorry

theorem myThm (p : P) (q : Q) (r : R) : False := sorry

example (q : Q) : False := by
  apply myThm ?_ q
  -- goals are now `R, P` **in that order**!

It seems that if apply is given input with explicit blanks ?_, it will put the goals for the explicit blanks after, not before, the goals it auto-generates -- which doesn't match the order of arguments for the lemma that's being invoked. This is troublesome because apply is otherwise pretty much synonymous with "refine with arbitrarily many blanks appended to the end".

Do others agree that it would be better if the above code returned the goals P, R not R, P?

[Weiyi Wang]

I discovered this the other day, and I decided for myself if I am going to have ?_ I always use refine so I don't get confused