[Agda] Bounties for Agda features

[Nils Anders Danielsson]

On 2012-05-07 21:33, Andreas Abel wrote:
> Well, a simple heuristics would be to only unfold definitions when
> making progress, where progress means that a constructor-pattern
> matched and an equation fired.
>
> Unfortunately, that would still destroy your beautiful 1 + x.
>
> However,  Data.List's
>
>    any p xs
>
> would not be unfolded to
>
>    foldr _v_ false (map p xs).
>
> Which would already be something.

You can control the amount of unfolding in the output:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations

If you use the "without normalising" variants, then things are often
less unfolded.

Tomas Hallgren mentioned to me that it can be a problem that
meta-variables are instantiated with unfolded terms. Perhaps we should
store two copies of terms, one with minimal unfolding and one which
records the unfolding that we have already performed (to avoid
recomputing things).

-- 
/NAD