Closed Seasawher closed 1 day ago
マクロではない! ちょっと意外だね
example (a b : Nat) (h : a = b + 0) : a = b := by
set_option trace.Elab.step true in
/-
[Elab.step] simpa using h ▼
[] simpa using h ▼
[] simpa using h ▼
[] expected type: <not-available>, term
h ▼
[result] h
[] expected type: a = b, term
h✝ ▼
[result] h✝
-/
simpa using h
検証して、マクロならそう書く