r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix: arity in the extern attribute

main
Henrik Böving 2022-02-16 21:24:42 +01:00
parent 7d43c83178
commit 28dfc14530
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
DocGen4/Attributes.lean
View File

@ -66,7 +66,7 @@ instance : ToString ExternEntry where
| ExternEntry.foreign backend fn => s!"{backend} foreign {fn}" | ExternEntry.foreign backend fn => s!"{backend} foreign {fn}"
instance : ToString ExternAttrData where instance : ToString ExternAttrData where
toString data := (data.arity?.map toString |>.getD "") ++ String.intercalate " " (data.entries.map toString) 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⟩]