rewrite with the goal

Stream: lean4

[Aaron Liu]

This is probably not supposed to happen

set_option pp.instantiateMVars false

example : 1 = 2 := by
  -- error: don't know how to synthesize placeholder
  refine ?k
  -- trying to print the term will stack overflow
  -- show_term
  rw [?k]

[Aaron Liu]

(you're also not supposed to rewrite the goal with itself, but that's not the point)

[Robin Arnez]

Wow, the one thing I forgot to mention about simpa:

/--
error: Occurs check failed: Expression
  ?k
contains the goal ?k
-/
#guard_msgs in
example : 1 = 2 := by
  refine ?k
  simpa using ?k

[Aaron Liu]

yes, that was the inspiration :)

[Aaron Liu]

cases also seems to have this problem

example : 1 = 2 := by
  refine ?k
  cases ?k

[Kyle Miller]

The occurs check in simpa is almost a year old. There are plenty more examples of this bug out there!

[Kyle Miller]

lean4#10306 adds an occurs check for rw