Merge pull request #815 from lean-ja/Seasawher/issue284

`[inherit_doc]` を紹介する

Examples/Command/Attribute/InheritDoc.lean

@@ -0,0 +1,36 @@
+/- # inherit_doc
+`inherit_doc` 属性を指定すると、既存の定数などのドキュメントコメントを使いまわすことができます。
+-/
+import Lean
+
+open Lean
+
+/-- 最初に与えた doc コメント -/
+def greet := "hello"
+
+-- `greet` のドキュメントコメントを引き継ぐ
+@[inherit_doc greet] abbrev greet' := greet
+
+section
+
+open Elab.Command
+
+/-- ドキュメントコメントを取得して表示するコマンド -/
+elab "#doc " x:ident : command => do
+  let name ← liftCoreM do realizeGlobalConstNoOverload x
+  if let some s ← findDocString? (← getEnv) name then
+  logInfo m!"{s}"
+
+end
+
+/-- info: 最初に与えた doc コメント -/
+#guard_msgs in #doc greet'
+
+/- `inherit_doc` を使用するのは、記法を導入する際であることが多いでしょう。この場合、ドキュメントコメントの継承元を指定する必要がありません。 -/
+
+/-- `⊔` という記号のための型クラス -/
+class Sup (α : Type) where
+  /-- 最小上界、上限 -/
+  sup : α → α → α
+
+@[inherit_doc] infixl:68 " ⊔ " => Sup.sup

src/SUMMARY.md

@@ -63,6 +63,7 @@
     - [cases_eliminator: 独自場合分け](./Command/Attribute/CasesEliminator.md)
     - [csimp: 効率的な実装に置換](./Command/Attribute/Csimp.md)
     - [induction_eliminator: 独自帰納法](./Command/Attribute/InductionEliminator.md)
+    - [inherit_doc: ドキュメントの継承](./Command/Attribute/InheritDoc.md)
     - [simps: simp補題の自動生成](./Command/Attribute/Simps.md)
 
 - [タクティク](./Tactic/README.md)