feat: export attribute

2022-04-12 19:09:42 +02:00 · 2022-04-12 19:09:42 +02:00 · ea66f7f243
parent 2128e789ca
commit ea66f7f243
1 changed files with 1 additions and 1 deletions
--- 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