doc: refine rwa docstring (#5811)

fixes #5792
leanprover · Oct 22, 2024 · eddbdd7 · eddbdd7
1 parent f0c1902
commit eddbdd7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
@@ -495,7 +495,7 @@ macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
     `(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
   | _ => Macro.throwUnsupported
 
-/-- `rwa` calls `rw`, then closes any remaining goals using `assumption`. -/
+/-- `rwa` is short-hand for `rw; assumption`. -/
 macro "rwa " rws:rwRuleSeq loc:(location)? : tactic =>
   `(tactic| (rw $rws:rwRuleSeq $[$loc:location]?; assumption))