[Agda] Bounties for Agda features

[Peter Hancock]

It seems to me this dream of selecting the "best" presentation of
something like a type in the current context is fantasy, and would amount to
Super Cow Powers or mind-reading or solving the halting problem.

But it is a very enticing fantasy, as any one will agree who has
spent time massaging pieces of text spat out by Agda into an intelligible form.
This seems to be mostly introducing "beta-expansions" and
local definitions, or (re-)factoring in some sense.

Some crude control over how the same thing is presented in different contexts
might be worthwhile if it cost next to nothing.

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