-- 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.
This gives an
unexpected end of inputon the last line. It's not related to it being->; other intro patterns result in the same error. Moving themove=>->line abovetrace_state, the error disappears, so it seems inherently related to this being the last tactic in a proof.