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

chore: print named instance arguments

main
Henrik 2023-09-10 00:18:52 +02:00
parent 36e1b863a7
commit 8ea6a55a82
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/Process/NameInfo.lean
View File

@ -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 -- and print what is left after the : instead. The only exception
-- to this is instances since these almost never have a name -- to this is instances since these almost never have a name
-- but should still be printed as arguments instead of after the :. -- 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 arg := (none, type, data)
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩)) let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
(#[arg] ++ args, final) (#[arg] ++ args, final)