Unexpected end of input

[dranov]

-- Left rewrite
theorem lrw_intro_1 : ∀ (x y z : Nat), x = y → y = z → z = x := by
  move=>x y z <-
  trace_state
  move=>->

This gives an unexpected end of input on the last line. It's not related to it being ->; other intro patterns result in the same error. Moving the move=>-> line above trace_state, the error disappears, so it seems inherently related to this being the last tactic in a proof.