[Agda] Re: Bounties for Agda features

Thomas Hallgren hallgren at chalmers.se
Wed May 9 14:37:57 CEST 2012

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



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

More information about the Agda mailing list