search

Toxaris / pts

Interpreter for functional pure type systems.
BSD 3-Clause "New" or "Revised" License
21 stars 7 forks source link

Allow "_(" term ")" in the input syntax to request type inference #8

Closed Blaisorblade closed 11 years ago

Blaisorblade commented 11 years ago

The goal is to allow pretty-printing such subexpressions as simple underscores (or maybe as nothing, who knows?) for extra readability in LaTeX output.

However, don't change parens, since it is used in too many places. Changing parens would additionally allow things like:

f _(a b : type) ...

instead of

f (a b : type) ...

so add the _( ) syntax only to a variant of parens (which reuses the old code).

Toxaris commented 11 years ago

This only makes sense if lhs2tex can handle special formatting for "", which needs to be tested. Otherwise, we should rather use "ignore" instead of "".

Toxaris commented 11 years ago

I finally tried this, and the following works:

%format (_ (x)) = "\ldots"

> foo = bar (_(hidden argument)) visible

produces the following displayed code in the pdf:

foo = bar ... visible
Blaisorblade commented 11 years ago

Cool, thanks!