docs(tactic/algebra): Module docstring (#13571)

Write the module docstring.
leanprover-community · Apr 25, 2022 · 045fc44 · 045fc44
1 parent 54d1ddd
commit 045fc44
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/tactic/algebra.lean b/src/tactic/algebra.lean
@@ -5,6 +5,14 @@ Authors: Simon Hudon
 -/
 import tactic.core
 
+/-!
+# Recording typeclass ancestors
+
+The "old" structure command currently does not record the parent typeclasses. This file defines the
+`ancestor` attribute to remedy this. This information is notably used by `to_additive` to map
+structure fields and constructors of a multiplicative structure to its additive counterpart.
+-/
+
 open lean.parser
 
 namespace tactic