From 8ea6a55a82ecb27f1c5290c5249d8490af855d3a Mon Sep 17 00:00:00 2001
From: Henrik <hargonix@gmail.com>
Date: Sun, 10 Sep 2023 00:18:52 +0200
Subject: [PATCH] chore: print named instance arguments

---
 DocGen4/Process/NameInfo.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/DocGen4/Process/NameInfo.lean b/DocGen4/Process/NameInfo.lean
index f567fe5..8cb0ed8 100644
--- a/DocGen4/Process/NameInfo.lean
+++ b/DocGen4/Process/NameInfo.lean
@@ -21,7 +21,7 @@ partial def typeToArgsType (e : Expr) : (Array ((Option Name) × Expr × BinderI
     -- and print what is left after the : instead. The only exception
     -- to this is instances since these almost never have a name
     -- but should still be printed as arguments instead of after the :.
-    if data.isInstImplicit then
+    if data.isInstImplicit && name.hasMacroScopes then
       let arg := (none, type, data)
       let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
       (#[arg] ++ args, final)