goal at the end of `simp at`

Stream: lean4

[Horațiu Cheval]

It seems that ⊢ can only be placed last in the list of a simp at tactic call.

example (h h' : True) : True ∧ False := by
  simp at h ⊢ h'
-- unknown tactic

but simp at h h' ⊢ works. Is this by design?

[Mario Carneiro]

It's a pretty meaningless piece of syntax flexibility