[Agda] Re: Bounties for Agda features

[Thomas Hallgren]

Alfa offered a lot of control over how terms were presented, see

	http://www.cse.chalmers.se/~hallgren/Alfa/Tutorial/GFplugin.html
	http://www.cse.chalmers.se/~hallgren/Papers/lpar2000.ps.gz

	http://www.cse.chalmers.se/~hallgren/Alfa/userguide.html#layout
	http://www.cse.chalmers.se/~hallgren/Alfa/Tutorial/ndstyle.html

But this is orthogonal to how you control how far terms are unfolded...

Thomas H

On 2012-05-09 0:09 , Peter Hancock wrote:
> A system I used long ago called alfa
> by Thomas Hallgren used to offer some control of this kind for a primeval
> version of agda.
> Exaggerating slightly, you could ask to see your type-expression written in
> latin or punched-card
> notation, using code contributed by Aarne Ranta.
> 
> Peter Hancock