Both implicit and explicit arguments are printed within parenthesis (no curly braces), using the prettyTel function in src/Tog/Abstract.
I tried working on printing implicit arguments within curly braces, but I believe at some point Tog throws away the hidden binding information and deal with implicit and explicit arguments the same way, adding _ in places where a hidden argument is not passed. Here are some more details:
Implicit arguments are defined using HBind constructor of the Binding type. They are part of the abstract syntax that result from the parser, which is defined in bnfc/Tog/Raw/Abs.
The scope checker converts the syntax into a smaller abstract tree defined in src/Tog/Abstract. It is not clear to me how this translation deal with HBind. Investigating the code in Tog.ScopeChecker, I understand it gets translated to a Hidden type, but it is not clear to me how the system deals with it.
Both implicit and explicit arguments are printed within parenthesis (no curly braces), using the
prettyTelfunction insrc/Tog/Abstract.I tried working on printing implicit arguments within curly braces, but I believe at some point Tog throws away the hidden binding information and deal with implicit and explicit arguments the same way, adding
_in places where a hidden argument is not passed. Here are some more details:HBindconstructor of the Binding type. They are part of the abstract syntax that result from the parser, which is defined inbnfc/Tog/Raw/Abs.src/Tog/Abstract. It is not clear to me how this translation deal withHBind. Investigating the code inTog.ScopeChecker, I understand it gets translated to aHiddentype, but it is not clear to me how the system deals with it.