[Agda] How to show a Term?

[Ulf Norell]

You can define showTerm yourself. The only annoying part is that fixity
information is currently not available for names (see
https://github.com/agda/agda/issues/1664), so you would need to pretty
print some superfluous parens.

/ Ulf

On Sat, Jul 23, 2016 at 7:19 PM, Roman <effectfully at gmail.com> wrote:

> Hi. `unquote` allows to print a Term, but it also performs type
> checking. Is there a way to print a Term just like `unquote` does, but
> without type checking it? I.e. something like `showTerm : Term ->
> String`. It's hard to read plain Terms even with appropriate {-#
> DISPLAY #-} pragmas and more importantly we could define a type class
>
> record Quote {α} (A : Set α) : Set α where
>   field deepQuote : A -> Term
>
>   show : A -> String
>   show = showTerm ∘ deepQuote
> open Quote {{...}} public
>
> instead of the Show type class and delegate pretty printing to the
> built-in machinery therefore avoiding all the burden of dealing with
> associativity, inserting parentheses and spaces etc.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160802/39f0d3ca/attachment.html