[Agda] PrettyPrint.agda

[Yoriyuki Yamagata]

Hi, Nils and list

I have updated PrettyPrint.agda and make internal definitions private.

Nils Anders Danielsson さんは書きました:
> On Wed, Aug 27, 2008 at 04:30, Yoriyuki Yamagata
> <yoriyuki.yamagata at aist.go.jp> wrote:
>   
>> Thank you for the suggestion.  I will look to them.
>>     
>
> I think that the latest version of Olaf Chitil's pretty-printing
> library should be relatively easy to port:
>
>   http://www.cs.kent.ac.uk/people/staff/oc/pretty.html
>
> A quick inspection of the source code indicates that all you need to
> do in order to please the termination and coverage checkers is to add
> a size index to the deque type.
>
>   

Thanks again for the suggestion, but since PrettyPrint.agda is a part of 
larger project, I leave it as it for now.  If the problem of the current 
implementation become apparent, I will consider another implementation.


-- 
Yoriyuki Yamagata (Research Scientist)
National Institute of Advanced Industrial Science and Technology
E-mail: yoriyuki.yamagata at aist.go.jp
Tel:+81-6-4863-5036 FAX:+81-6-4863-5052
http://staff.aist.go.jp/yoriyuki.yamagata/index.html.en