- Comments are appropriate when a Lean tactic has a name that does not clearly indicate its meaning. - Lean `coding phrases` that are self-explanatory are appropriate, such as using: - [[exact-show|exact]] *Goal* from *Hypothesis* instead of exact *Hypotheses*. - A set of [[LeanNotes coding macros|macros]] can be useful to streamline the uniform application of comments. --- Author: [[dducoff]] Posted Date: 2026-06-25