calc mode in a subgoal

Stream: lean4

[Riccardo Brasca]

I want to use calc in a subgoal, but a get a strange error in the following goal

example (a b a' b' : Nat) (ha : a = a') (hb : b = b') : a = a' ∧ b = b' := by
  constructor
  · calc a = a' := by exact ha
  · assumption -- error: unexpected end of input; expected ':='

On the other hand, the following works

example (a b a' b' : Nat) (ha : a = a') (hb : b = b') : a = a' ∧ b = b' := by
  constructor
  { calc a = a' := by exact ha }
  · assumption

What am I doing wrong?

[Ruben Van de Velde]

Does it only happen if you have a single line (useless) calc?

[Riccardo Brasca]

Ah, yes!

example (a b a' b' : Nat) (ha : a = a') (hb : b = b') : a = a' ∧ b = b' := by
  constructor
  · calc a = a := rfl
    _ = a' := ha
  · assumption

is ok

[Ruben Van de Velde]

I'm more surprised your other code does work