From ea66f7f243bb8a4b0872739d5b37e7423ab255a8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 12 Apr 2022 19:09:42 +0200
Subject: [PATCH] feat: export attribute

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

diff --git a/DocGen4/Attributes.lean b/DocGen4/Attributes.lean
index eebe213..2e30789 100644
--- a/DocGen4/Attributes.lean
+++ b/DocGen4/Attributes.lean
@@ -68,7 +68,7 @@ instance : ToString ExternEntry where
 instance : ToString ExternAttrData where
   toString data := (data.arity?.map toString |>.getD "") ++ " " ++ String.intercalate " " (data.entries.map toString)
 
-def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩]
+def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩, ⟨exportAttr⟩]
 
 def getTags (decl : Name) : MetaM (Array String) := do
   let env ← getEnv