Introing hypotheses and lets simultaneously

Stream: lean4

[Bolton Bailey]

Here is an MWE

example : (a : ℕ) -> (b : ℕ) ->
  let c := a + b ; c = b + a := by
  -- intros -- works, but no names
  -- intros a b ; intros hc -- works, but takes two invocations
  intros a b hc --tactic 'introN' failed, insufficient number of binders

Is this a bug?

[Thomas Murrills]

This doesn’t fail on lean web for me currently. What version of lean are you on?

[Bolton Bailey]

I am unfortunately in an update which is going horribly wrong, so I'm not sure anymore, sorry. 4.3.0 potentially?

[Kyle Miller]

It works for me locally,

#eval Lean.versionString -- "4.3.0"