From 1f081ee6cb776b0dcf0de8aba0da04712d2867aa Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 22 Jul 2022 13:36:53 +0200
Subject: [PATCH] feat: doc comment support for `unif_hint`

---
 src/Init/NotationExtra.lean   | 6 +++---
 tests/lean/run/unifhint1.lean | 1 +
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 493a86dc2f..d5b66bd939 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -64,15 +64,15 @@ def expandBrackedBinders (combinatorDeclName : Name) (bracketedExplicitBinders :
 syntax unifConstraint := term (" =?= " <|> " ≟ ") term
 syntax unifConstraintElem := colGe unifConstraint ", "?
 
-syntax attrKind "unif_hint " (ident)? bracketedBinder* " where " withPosition(unifConstraintElem*) ("|-" <|> "⊢ ") unifConstraint : command
+syntax (docComment)? attrKind "unif_hint " (ident)? bracketedBinder* " where " withPosition(unifConstraintElem*) ("|-" <|> "⊢ ") unifConstraint : command
 
 macro_rules
-  | `($kind:attrKind unif_hint $(n)? $bs:bracketedBinder* where $[$cs₁:term ≟ $cs₂]* |- $t₁:term ≟ $t₂) => do
+  | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁:term ≟ $cs₂]* |- $t₁:term ≟ $t₂) => do
     let mut body ← `($t₁ = $t₂)
     for (c₁, c₂) in cs₁.zip cs₂ |>.reverse do
       body ← `($c₁ = $c₂ → $body)
     let hint : Ident ← `(hint)
-    `(@[$kind:attrKind unificationHint] def $(n.getD hint):ident $bs:bracketedBinder* : Sort _ := $body)
+    `($[$doc?:docComment]? @[$kind:attrKind unificationHint] def $(n.getD hint) $bs:bracketedBinder* : Sort _ := $body)
 end Lean
 
 open Lean
diff --git a/tests/lean/run/unifhint1.lean b/tests/lean/run/unifhint1.lean
index 5cad7fcd43..9e0c05917e 100644
--- a/tests/lean/run/unifhint1.lean
+++ b/tests/lean/run/unifhint1.lean
@@ -16,6 +16,7 @@ instance : CoeSort Magma.{u} (Type u) where
 def mul {s : Magma} (a b : s) : s :=
   s.mul a b
 
+/-- hi -/
 unif_hint (s : Magma) where
   s =?= Nat.Magma |- s.α =?= Nat